Commit 2024-11-03 08:14 6f9adc71

View on Github →

feat(GroupTheory/OrderOfElement): If a ≤ g • a, then g • a = a (#17752) This PR adds a few lemmas about group actions on partial orders.

Estimated changes

added theorem le_pow_smul
added theorem pow_smul_le
added theorem smul_eq_of_le_smul
added theorem smul_eq_of_smul_le