Theorem Subgroup.pi_mem_of_mulSingle_mem_aux

Modification history

2026-04-17 09:59
Mathlib/Algebra/Group/Subgroup/Finite.lean
chore: remove declarations deprecated between 2021-04-15 and 2025-10-15 (#38057) …
Deleted Subgroup.pi_mem_of_mulSingle_mem_auxView on Github →
2023-01-30 19:17
Mathlib/GroupTheory/Subgroup/Finite.lean
feat: port GroupTheory.Subgroup.Finite (#1864) …
Added Subgroup.pi_mem_of_mulSingle_mem_auxView on Github →