Theorem Valuation.IsEquiv.orderMonoidIso_spec₀

Modification history

2026-08-01 16:40

Mathlib/RingTheory/Valuation/Basic.lean

chore(RingTheory/Valuation/Basic): remove all `set_option`s in this file (#42335)

Added Valuation.IsEquiv.orderMonoidIso_spec₀ View on Github →