English
In a finite-dimensional extension L/K with valuation v, if x ∈ L is a unit, then a certain power of the valuation of the constant term of the minimal polynomial of x is nonzero.
Русский
В конечноразмерном расширении L/K с valuations v, если x ∈ L является единицей, то соответствующая степень отношение v константы минимального многочлена x не равна нулю.
LaTeX
$$$\\text{FiniteDimensional}_K L \\Rightarrow (\\exists x\\in L\\text{ with } \\text{IsUnit}(x) ) \\Rightarrow v((\\minpoly_K x).coeff 0)^{\\frac{\\mathrm{finrank}_K L}{(\\minpoly_K x).natDegree}} \\neq 0.$$$
Lean4
theorem pow_coeff_zero_ne_zero_of_unit [FiniteDimensional K L] (x : L) (hx : IsUnit x) :
v ((minpoly K x).coeff 0) ^ (finrank K L / (minpoly K x).natDegree) ≠ (0 : Γ₀) :=
by
have h_alg : Algebra.IsAlgebraic K L := Algebra.IsAlgebraic.of_finite K L
have hx₀ : IsIntegral K x := (Algebra.IsAlgebraic.isAlgebraic x).isIntegral
have hdeg := Nat.div_pos (natDegree_le x) (natDegree_pos hx₀)
rw [ne_eq, pow_eq_zero_iff hdeg.ne.symm, Valuation.zero_iff]
exact coeff_zero_ne_zero hx₀ hx.ne_zero
