Theorem Valuation.ne_zero_of_isUnit

Modification history

2024-08-26 11:39

Mathlib/RingTheory/Valuation/Basic.lean

feat(RingTheory.Valuation.Minpoly): add valuation lemmas (#15736) …

Added Valuation.ne_zero_of_isUnit View on Github →