Commit 2024-11-13 18:58 3d1502cf

View on Github →

chore(Subgroup/ZPowers): split (#18828)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/CharZero/Quotient.lean

Renamed Mathlib/Algebra/Group/Subgroup/ZPowers.lean to Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean

deleted theorem AddSubgroup.intCast_mem_zmultiples_one

deleted theorem AddSubgroup.intCast_mul_mem_zmultiples

deleted theorem AddSubgroup.range_zmultiplesHom

deleted theorem Int.range_castAddHom

deleted theorem Subgroup.center_eq_iInf

deleted theorem Subgroup.center_eq_infi'

deleted theorem Subgroup.centralizer_closure

deleted theorem Subgroup.range_zpowersHom

Created Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean

added theorem AddSubgroup.intCast_mem_zmultiples_one

added theorem AddSubgroup.intCast_mul_mem_zmultiples

added theorem AddSubgroup.range_zmultiplesHom

added theorem Int.range_castAddHom

added theorem Subgroup.center_eq_iInf

added theorem Subgroup.center_eq_infi'

added theorem Subgroup.centralizer_closure

added theorem Subgroup.range_zpowersHom

Modified Mathlib/Algebra/ModEq.lean

Modified Mathlib/Algebra/Periodic.lean

Modified Mathlib/GroupTheory/GroupAction/ConjAct.lean

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean