Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-19 10:01 72224634

View on Github →

chore(algebra/iterate_hom): use to_additive to fill missing lemmas (#10886)

Estimated changes

Modified src/algebra/iterate_hom.lean

added theorem add_monoid.End.coe_pow

deleted theorem add_monoid_hom.iterate_map_sub

added theorem monoid.End.coe_pow

added theorem monoid_hom.iterate_map_div

modified theorem monoid_hom.iterate_map_pow

modified theorem monoid_hom.iterate_map_zpow