Theorem LocalizedModule.oreEqv_eq_r

Modification history

2025-12-28 17:51
Mathlib/Algebra/Module/LocalizedModule/Basic.lean
chore: unify `LocalizedModule` and `OreLocalization` (#31862) …
Added LocalizedModule.oreEqv_eq_rView on Github →