Commit 2024-06-05 08:10 3b9aaf4f

View on Github →

refactor: Redefine pow in terms of iterate (#1388) In the Monoid instances for Function.End α, Equiv.Perm α, Monoid.End α, AddMonoid.End α, α →+* α, replace the default npowRec by a custom one in terms of Nat.iterate. Write the expected coercion lemmas. As a consequence, I can delete the recently introduced file Algebra.Ring.Hom.IterateHom. Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.231388.20Redefine.20pow.20in.20terms.20of.20iterate

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Action/Defs.lean

Modified Mathlib/Algebra/Group/Hom/Defs.lean

added theorem AddMonoid.End.coe_mul

added theorem AddMonoid.End.coe_one

added theorem AddMonoid.End.coe_pow

deleted theorem AddMonoid.coe_mul

deleted theorem AddMonoid.coe_one

added theorem Monoid.End.coe_pow

Modified Mathlib/Algebra/GroupPower/IterateHom.lean

deleted theorem AddMonoid.End.coe_pow

deleted theorem Monoid.End.coe_pow

deleted theorem MonoidHom.coe_pow

Modified Mathlib/Algebra/Ring/Hom/Defs.lean

modified theorem RingHom.coe_mul

modified theorem RingHom.coe_one

added theorem RingHom.coe_pow

modified theorem RingHom.mul_def

modified theorem RingHom.one_def

Deleted Mathlib/Algebra/Ring/Hom/IterateHom.lean

deleted theorem RingHom.coe_pow

Modified Mathlib/Dynamics/FixedPoints/Basic.lean

Modified Mathlib/GroupTheory/Perm/Basic.lean

modified theorem Equiv.Perm.coe_pow

modified theorem Equiv.Perm.iterate_eq_pow