Commit 2023-09-28 12:57 edaa10ad

View on Github →

feat(GroupTheory/Submonoid): add opposite submonoids (#7415) We already have API for the multiplicative opposite of subgroups. This tidies the API for subgroups by introducing separate .op and .unop definitions (as dot notation on .opposite worked in Lean 3 but not Lean 4), and adds the same API for submonoids.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/GroupTheory/Coset.lean

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

Modified Mathlib/GroupTheory/Subgroup/MulOpposite.lean

added def Subgroup.equivOp

added def Subgroup.opEquiv

added theorem Subgroup.op_toSubmonoid

deleted def Subgroup.opposite

deleted def Subgroup.oppositeEquiv

modified theorem Subgroup.smul_opposite_mul

added theorem Subgroup.unop_toSubmonoid

Modified Mathlib/GroupTheory/Subgroup/Pointwise.lean

modified theorem Subgroup.smul_opposite_image_mul_preimage

Created Mathlib/GroupTheory/Submonoid/MulOpposite.lean

added def Submonoid.equivOp

added def Submonoid.opEquiv

Modified Mathlib/MeasureTheory/Integral/Periodic.lean

Modified Mathlib/MeasureTheory/Measure/Haar/Quotient.lean

Modified Mathlib/Topology/Algebra/Group/Basic.lean

Modified Mathlib/Topology/Instances/AddCircle.lean