Commit 2026-08-01 16:40 cb48454a

View on Github →

chore(RingTheory/Valuation/Basic): remove all set_options in this file (#42335)

Estimated changes

Modified Mathlib/RingTheory/Valuation/Basic.lean

added theorem Valuation.IsEquiv.ofClass_eq_zero

added theorem Valuation.IsEquiv.orderMonoidIso_spec₀

modified theorem Valuation.IsEquiv.valueGroup₀Fun_spec

added theorem Valuation.OrderMonoidWithZeroHom.ofClass_monotone

modified theorem Valuation.isEquiv_restrict

modified theorem Valuation.restrict_inj

Modified Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean