mathlib

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