Commit 2025-08-20 03:43 cb7220f9

View on Github →

chore(Algebra/Group): rename Nat.addSubmonoid_closure_one and AddSubgroup.closure_singleton_int_one_eq_top (#28301) This PR renames Nat.addSubmonoid_closure_one to Nat.addSubmonoidClosure_one, and AddSubgroup.closure_singleton_int_one_eq_top to Int.addSubgroupClosure_one, to align with naming convention. It also deprecates AddSubgroup.zmultiples_one_eq_top because it's duplication of existing Int.zmultiples_one, and simplifies the proof of AddGroup.FG ℤ using the renamed theorem.

Estimated changes

Modified Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean

deleted theorem AddSubgroup.closure_singleton_int_one_eq_top

deleted theorem AddSubgroup.zmultiples_one_eq_top

added theorem Int.addSubgroupClosure_one

Modified Mathlib/Algebra/Group/Submonoid/Operations.lean

added theorem Nat.addSubmonoidClosure_one

deleted theorem Nat.addSubmonoid_closure_one

Modified Mathlib/Algebra/Order/Star/Basic.lean

Modified Mathlib/GroupTheory/ArchimedeanDensely.lean

Modified Mathlib/GroupTheory/Finiteness.lean