Commit 2023-10-03 10:19 71442323

View on Github →

feat: sup_eq_closure for Submonoid and Subgroup (#7468)

Estimated changes

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

added theorem Subgroup.sup_eq_closure

Modified Mathlib/GroupTheory/Subgroup/Pointwise.lean

deleted theorem Subgroup.sup_eq_closure

added theorem Subgroup.sup_eq_closure_mul

Modified Mathlib/GroupTheory/Submonoid/Basic.lean

added theorem Submonoid.sup_eq_closure

Modified Mathlib/GroupTheory/Submonoid/Pointwise.lean

deleted theorem Submonoid.sup_eq_closure

added theorem Submonoid.sup_eq_closure_mul