Minimal polynomials.

We prove some results about valuations of zero coefficients of minimal polynomials.

Let K be a field with a valuation v and let L be a field extension of K.

Main statements

• coeff_zero_minpoly : for x ∈ K the valuation of the zeroth coefficient of the minimal polynomial of algebraMap K L x over K is equal to the valuation of x.
• pow_coeff_zero_ne_zero_of_unit : for any unit x : Lˣ, we prove that a certain power of the valuation of zeroth coefficient of the minimal polynomial of x over K is nonzero. This lemma is helpful for defining the valuation on L inducing v.

@[simp]

theorem Valuation.coeff_zero_minpoly {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) (L : Type u_3) [Field L] [Algebra K L] (x : K) : v ((minpoly K ((algebraMap K L) x)).coeff 0) = v x

For x ∈ K the valuation of the zeroth coefficient of the minimal polynomial of algebraMap K L x over K is equal to the valuation of x.

theorem Valuation.pow_coeff_zero_ne_zero_of_unit {K : Type u_1} [Field K] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀) {L : Type u_3} [Field L] [Algebra K L] [FiniteDimensional K L] (x : L) (hx : IsUnit x) : v ((minpoly K x).coeff 0) ^ (Module.finrank K L / (minpoly K x).natDegree) ≠ 0

For any unit x : Lˣ, we prove that a certain power of the valuation of zeroth coefficient of the minimal polynomial of x over K is nonzero. This lemma is helpful for defining the valuation on L inducing v.