Theorem Function.Surjective.preValuationRing

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 Function.Surjective.preValuationRingView on Github →