Theorem Valuation.IsEquiv.ne_zero

Modification history

2026-08-11 12:14
Mathlib/RingTheory/Valuation/Basic.lean
chore: delete deprecated declarations/modules from January 2026 (#42075) …
Deleted Valuation.IsEquiv.ne_zeroView on Github →
2026-01-25 15:24
Mathlib/RingTheory/Valuation/Basic.lean
feat(ValuationSubring): eq_top_iff + qol changes (#33604) …
Modified Valuation.IsEquiv.ne_zeroView on Github →
2023-03-17 12:44
Mathlib/RingTheory/Valuation/Basic.lean
feat: port RingTheory.Valuation.Basic (#2846)
Added Valuation.IsEquiv.ne_zeroView on Github →