Theorem PreValuationRing.cond

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.cond View on Github →