Def subgroupOfIdempotent

Modification history

2024-02-14 18:23

Mathlib/GroupTheory/OrderOfElement.lean

chore(OrderOfElement,Sylow): `Fintype` -> `Finite` (#10550)

Modified subgroupOfIdempotent View on Github →

2023-08-10 19:52

Mathlib/GroupTheory/OrderOfElement.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified subgroupOfIdempotent View on Github →

2023-02-22 16:34

Mathlib/GroupTheory/OrderOfElement.lean

feat: port GroupTheory.OrderOfElement (#2279)

Added subgroupOfIdempotent View on Github →