Theorems · Theorem · field theory

Valuation.coeff_zero_minpoly

∀ {K : Type u_1} [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀)
  (L : Type u_3) [inst_2 : Field L] [inst_3 : 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.

Defined in

Mathlib.RingTheory.Valuation.Minpoly

Cited by

0 results in Mathlib

Foundations

Depth 123 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldLinearOrderedCommGroupWithZeroFieldAlgebra