Theorem ValuationRing.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) …

Modified ValuationRing.iff_ideal_total View on Github →

2023-06-06 12:22

Mathlib/RingTheory/Valuation/ValuationRing.lean

feat: port RingTheory.Valuation.ValuationRing (#4720)

Added ValuationRing.iff_ideal_total View on Github →