Theorem smul_eq_of_le_smul

Modification history

2024-11-03 08:14
Mathlib/GroupTheory/OrderOfElement.lean
feat(GroupTheory/OrderOfElement): If `a ≤ g • a`, then `g • a = a` (#17752) …
Added smul_eq_of_le_smulView on Github →