Theorem Submonoid.iSup_map_mulSingle_le

Modification history

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