Commit 2024-10-04 20:24 4e011876
View on Github →chore(RingTheory/Valuation): change implicitness in Valuation.IsEquiv lemmas (#17051)
Generalize a suggestion mentioned here. Change (v v') to {v v'} and add aliases for easier application of these Valuation.IsEquivlemmas. Add an equivalent condition in Valuation.isEquiv_tfae.