Theorem RingEquiv.coe_coe_toMulEquiv_symm

Modification history

2026-04-19 10:51
Mathlib/Algebra/Ring/Equiv.lean
chore(Algebra/Category): add `ModuleCat.restrictScalarsIsoOfEquiv` (#37773) …
Added RingEquiv.coe_coe_toMulEquiv_symmView on Github →