Commit 2024-05-13 14:42 7384a70a

View on Github →

chore: Delete Algebra.GroupPower.Hom (#12817) After #12736, powMonoidHom and zpowGroupHom can move to Algebra.Group.Hom.Basic at no cost. This PR moves them and deletes the now empty Algebra.GroupPower.Hom.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Multiset/Basic.lean

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

added def powMonoidHom

added def zpowGroupHom

Deleted Mathlib/Algebra/GroupPower/Hom.lean

deleted def powMonoidHom

deleted def zpowGroupHom

Modified Mathlib/Algebra/GroupPower/Ring.lean