Theorem Submonoid.iSup_map_mulSingle

Modification history

2025-09-01 08:25
Mathlib/GroupTheory/Finiteness.lean
feat(GroupTheory/Finiteness): `Monoid.FG (∀ i, M i)` and `Group.FG (∀ i, M i)` (#28670) …
Added Submonoid.iSup_map_mulSingleView on Github →