Def ValuationSubring.toLocalSubring

Modification history

2024-11-14 17:15

Mathlib/RingTheory/Valuation/LocalSubring.lean

feat(RingTheory): valuation subrings are maximal local subrings (#19012) …

Added ValuationSubring.toLocalSubring View on Github →