Division_Theorem_for_Polynomial_Forms_over_Field
Proveddivisionfieldpolynomialproofwikiring-theory
Let be a field whose zero is and whose unity is . Let be transcendental over . Let be the ring of polynomials in over . Let be an element of of degree . Then such that either or and has degree that is less than .
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.RingTheory.Polynomial.Basic
Formal statement
theorem Division_Theorem_for_Polynomial_Forms_over_Field {F : Type _} [Field F] (f g : Polynomial F) (hg : g ≠ 0) : ∃ q r : Polynomial F, f = g * q + r ∧ (r = 0 ∨ r.natDegree < g.natDegree) := by sorrySource