Commit 2022-12-22 08:50 70613387

View on Github →

feat: port Algebra.Hom.Iterate (#1133)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Hom/Iterate.lean

added theorem AddMonoid.End.coe_pow

added theorem AddMonoidHom.iterate_map_smul

added theorem AddMonoidHom.iterate_map_zsmul

added theorem Commute.function_commute_mul_left

added theorem Commute.function_commute_mul_right

added theorem Equiv.Perm.coe_pow

added theorem Monoid.End.coe_pow

added theorem MonoidHom.coe_pow

added theorem MonoidHom.iterate_map_div

added theorem MonoidHom.iterate_map_inv

added theorem MonoidHom.iterate_map_mul

added theorem MonoidHom.iterate_map_one

added theorem MonoidHom.iterate_map_pow

added theorem MonoidHom.iterate_map_zpow

added theorem RingHom.coe_pow

added theorem RingHom.iterate_map_add

added theorem RingHom.iterate_map_mul

added theorem RingHom.iterate_map_neg

added theorem RingHom.iterate_map_one

added theorem RingHom.iterate_map_pow

added theorem RingHom.iterate_map_smul

added theorem RingHom.iterate_map_sub

added theorem RingHom.iterate_map_zero

added theorem RingHom.iterate_map_zsmul

added theorem SemiconjBy.function_semiconj_mul_left

added theorem SemiconjBy.function_semiconj_mul_right_swap

added theorem hom_coe_pow

added theorem mul_left_iterate

added theorem mul_right_iterate

added theorem mul_right_iterate_apply_one

added theorem pow_iterate

added theorem smul_iterate

added theorem zpow_iterate