Theorem Subgroup.toSubmonoid_zpowers

Modification history

2025-10-24 10:20

Mathlib/Algebra/Group/Subgroup/Pointwise.lean

chore(GroupTheory/Index): move awkwardly placed lemmas (#30832) …

Modified Subgroup.toSubmonoid_zpowers View on Github →

2025-09-29 19:11

Mathlib/GroupTheory/Index.lean

feat(GroupTheory): `powers_le_zpowers` (#29991) …

Added Subgroup.toSubmonoid_zpowers View on Github →