Commit 2025-07-06 01:40 95143f79
View on Github →chore(RingTheory/Valuation): Valution.Integers implies IsFractionRing (#26524)
generalize IsFractionRing v.integer K to IsFractionRing O K when v.Integers O K.
Since IsFractionRing is prop, one should have a prop-relationship between the valuation subring and base ring
On the way, remove IsDomain O from the necessary TC arguments, since it is implied by Valuation.Integers