Commit 2024-05-25 19:14 59150e2c

View on Github →

chore: Delete Algebra.GroupPower.Ring (#12957) Move the few remaining lemmas to earlier files.

Estimated changes

Modified Mathlib.lean

Deleted Mathlib/Algebra/GroupPower/Ring.lean

deleted theorem coe_powMonoidWithZeroHom

deleted def powMonoidWithZeroHom

deleted theorem powMonoidWithZeroHom_apply

deleted theorem pow_dvd_pow_iff

Modified Mathlib/Algebra/GroupWithZero/Divisibility.lean

added theorem pow_dvd_pow_iff

Modified Mathlib/Algebra/GroupWithZero/Hom.lean

added theorem coe_powMonoidWithZeroHom

added def powMonoidWithZeroHom

added theorem powMonoidWithZeroHom_apply

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

Modified Mathlib/Algebra/Order/Field/Defs.lean

Modified Mathlib/Algebra/Polynomial/Basic.lean

Modified Mathlib/Algebra/Ring/Divisibility/Lemmas.lean

Modified Mathlib/Data/Complex/Basic.lean

Modified Mathlib/Data/ENNReal/Operations.lean

Modified Mathlib/Data/ZMod/IntUnitsPower.lean

Modified Mathlib/GroupTheory/OrderOfElement.lean

Modified Mathlib/NumberTheory/FLT/Basic.lean

Modified Mathlib/RingTheory/Coprime/Basic.lean

Modified Mathlib/RingTheory/Multiplicity.lean

Modified Mathlib/Topology/Algebra/Field.lean