Commit 2024-03-27 09:30 137f088d

View on Github →

refactor(Algebra/GroupPower/IterateHom): Use HomClass to generalize map_iterate statements (#11266) This PR uses the HomClass architecture to generalize the map_iterate statements in Algebra/GroupPower/IterateHom.lean.

Estimated changes

Modified Mathlib/Algebra/CharP/ExpChar.lean

Modified Mathlib/Algebra/GroupPower/IterateHom.lean

deleted theorem AddMonoidHom.iterate_map_smul

deleted theorem AddMonoidHom.iterate_map_zsmul

deleted theorem MonoidHom.iterate_map_div

deleted theorem MonoidHom.iterate_map_inv

deleted theorem MonoidHom.iterate_map_one

deleted theorem MonoidHom.iterate_map_pow

deleted theorem MonoidHom.iterate_map_zpow

deleted theorem RingHom.iterate_map_neg

deleted theorem RingHom.iterate_map_one

deleted theorem RingHom.iterate_map_pow

deleted theorem RingHom.iterate_map_smul

deleted theorem RingHom.iterate_map_sub

deleted theorem RingHom.iterate_map_zero

deleted theorem RingHom.iterate_map_zsmul

added theorem iterate_map_div

added theorem iterate_map_inv

modified theorem iterate_map_mul

added theorem iterate_map_one

added theorem iterate_map_pow

added theorem iterate_map_zpow

Modified Mathlib/Analysis/InnerProductSpace/MeanErgodic.lean

Modified Mathlib/Data/Polynomial/Derivative.lean

modified theorem Polynomial.iterate_derivative_zero

Modified Mathlib/FieldTheory/PerfectClosure.lean

Modified Mathlib/RingTheory/Perfection.lean