Theorem Set.inv_mem_centralizer₀

Modification history

2024-07-10 17:26

Mathlib/Algebra/GroupWithZero/Center.lean

chore: Merge `Algebra.Group.Centralizer` into `Algebra.Group.Center` (#13034)

Modified Set.inv_mem_centralizer₀ View on Github →

2024-07-01 09:41

Mathlib/Algebra/Group/Centralizer.lean

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

Modified Set.inv_mem_centralizer₀ View on Github →

2024-04-20 06:50

Mathlib/Algebra/Group/Centralizer.lean

chore: refactor to avoid importing Ring for Group topics (#11913) …

Modified Set.inv_mem_centralizer₀ View on Github →

2023-01-02 20:39

Mathlib/GroupTheory/Subsemigroup/Centralizer.lean

feat: port GroupTheory.Subsemigroup.Centralizer (#1286) …

Added Set.inv_mem_centralizer₀ View on Github →