Theorem Valuation.ne_zero_of_unit

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_unitView on Github →