Commit 2024-01-16 00:56 b47d3300

View on Github →

chore: replace SubgroupClass.inv by InvMemClass.inv (#9761)

Estimated changes

Modified Mathlib/Algebra/Module/Submodule/Basic.lean

Modified Mathlib/Algebra/Module/Zlattice.lean

Modified Mathlib/Analysis/Convex/Cone/Extension.lean

Modified Mathlib/Data/Complex/Module.lean

Modified Mathlib/GroupTheory/DoubleCoset.lean

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

added theorem InvMemClass.coe_inv

deleted theorem SubgroupClass.coe_inv