Theorem Submonoid.le_comap_mulSingle_pi

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.le_comap_mulSingle_piView on Github →