Theorem pow_smul_le

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 pow_smul_le 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 pow_smul_le View on Github →