Theorem le_pow_smul

Modification history

2026-09-26 10:13

Mathlib/Algebra/Order/Group/Action.lean

feat(RingTheory/Ideal): the `⊥` and `⊤` cases of the pointwise action on ideals (#44070) …

Modified le_pow_smul View on Github →

2024-11-03 08:14

Mathlib/Algebra/Order/Group/Action.lean

feat(GroupTheory/OrderOfElement): If `a ≤ g • a`, then `g • a = a` (#17752) …

Added le_pow_smul View on Github →