Theorem InvMemClass.coe_inv

Modification history

2024-10-28 17:42
Mathlib/Algebra/Group/Subgroup/Basic.lean
chore(Algebra/Group/Subgroup): split off `Defs` file (#18340) …
Modified InvMemClass.coe_invView on Github →
2024-01-16 00:56
Mathlib/GroupTheory/Subgroup/Basic.lean
chore: replace SubgroupClass.inv by InvMemClass.inv (#9761)
Added InvMemClass.coe_invView on Github →