Commit 2024-07-01 09:41 0b99fccb

View on Github →

chore: move some lemmas to Algebra.GroupWithZero.Center (#13944) From #13034.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Center.lean

deleted theorem Set.center_units_eq

deleted theorem Set.center_units_subset

deleted theorem Set.div_mem_center₀

deleted theorem Set.inv_mem_center₀

deleted theorem Set.zero_mem_center

Modified Mathlib/Algebra/Group/Centralizer.lean

deleted theorem Set.div_mem_centralizer₀

deleted theorem Set.inv_mem_centralizer₀

deleted theorem Set.zero_mem_centralizer

Created Mathlib/Algebra/GroupWithZero/Center.lean

added theorem Set.center_units_eq

added theorem Set.center_units_subset

added theorem Set.div_mem_center₀

added theorem Set.div_mem_centralizer₀

added theorem Set.inv_mem_center₀

added theorem Set.inv_mem_centralizer₀

added theorem Set.zero_mem_center

added theorem Set.zero_mem_centralizer

Modified Mathlib/GroupTheory/Subgroup/Center.lean

Modified Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean