Theorem Valuation.IsEquiv.ne_zero

Modification history

2026-01-25 15:24

Mathlib/RingTheory/Valuation/Basic.lean

feat(ValuationSubring): eq_top_iff + qol changes (#33604) …

Modified Valuation.IsEquiv.ne_zero View on Github →

2023-03-17 12:44

Mathlib/RingTheory/Valuation/Basic.lean

feat: port RingTheory.Valuation.Basic (#2846)

Added Valuation.IsEquiv.ne_zero View on Github →