Theorem PreValuationRing.iff_ideal_total

Modification history

2024-11-01 21:17
Mathlib/RingTheory/Valuation/ValuationRing.lean
feat(RingTheory/Valuation): `PreValuationRing`: without `IsDomain R` on the prop `ValuationRing R` (#17634) …
Added PreValuationRing.iff_ideal_totalView on Github →