Theorem Submonoid.map_coe_toMulEquiv

Modification history

2025-03-30 21:32
Mathlib/Algebra/Group/Submonoid/Operations.lean
refactor(RingTheory): small `erw`-removing refactors to localizations (#23375) …
Added Submonoid.map_coe_toMulEquivView on Github →