Commit 2025-02-22 11:05 eb486ffc

View on Github →

chore(Algebra/GroupPower/IterateHom): move all lemmas earlier (#22132) All lemmas in this file belong earlier. This finally gets rid of the Algebra.GroupPower folder, notorious for having caused imports increases in the algebra library (see #11855 for full motivation).

Estimated changes

added theorem smul_iterate
added theorem smul_iterate_apply
added theorem hom_coe_pow
added theorem mul_left_iterate
added theorem mul_right_iterate
added theorem pow_iterate
added theorem zpow_iterate
added theorem iterate_map_div
added theorem iterate_map_inv
added theorem iterate_map_mul
added theorem iterate_map_one
added theorem iterate_map_pow
added theorem iterate_map_zpow
deleted theorem hom_coe_pow
deleted theorem iterate_map_div
deleted theorem iterate_map_inv
deleted theorem iterate_map_mul
deleted theorem iterate_map_one
deleted theorem iterate_map_pow
deleted theorem iterate_map_zpow
deleted theorem mul_left_iterate
deleted theorem mul_right_iterate
deleted theorem pow_iterate
deleted theorem smul_iterate
deleted theorem smul_iterate_apply
deleted theorem zpow_iterate
added theorem IsLeftRegular.pow
added theorem IsLeftRegular.pow_iff
added theorem IsRegular.pow
added theorem IsRegular.pow_iff
added theorem IsRightRegular.pow
added theorem IsRightRegular.pow_iff
deleted theorem IsLeftRegular.pow
deleted theorem IsLeftRegular.pow_iff
deleted theorem IsRegular.pow
deleted theorem IsRegular.pow_iff
deleted theorem IsRightRegular.pow
deleted theorem IsRightRegular.pow_iff