Commit 2024-08-26 11:39 70e05eb4

View on Github →

feat(RingTheory.Valuation.Minpoly): add valuation lemmas (#15736) We prove some results about valuations of zero coefficients of minimal polynomials.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Valuation/Basic.lean

added theorem Valuation.ne_zero_of_isUnit

added theorem Valuation.ne_zero_of_unit

Created Mathlib/RingTheory/Valuation/Minpoly.lean

added theorem Valuation.coeff_zero_minpoly

added theorem Valuation.pow_coeff_zero_ne_zero_of_unit