Theorem Set.add_mem_centralizer

Modification history

2024-04-20 06:50

Mathlib/Algebra/Ring/Centralizer.lean

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

Modified Set.add_mem_centralizer View on Github →

2023-01-02 20:39

Mathlib/GroupTheory/Subsemigroup/Centralizer.lean

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

Added Set.add_mem_centralizer View on Github →