Mathlib Map

Theorems · Definition · group theory

Set.centralizer

{M : Type u_1} → Set M → [Mul M] → Set M

The centralizer of a subset of a magma.

Defined in
Mathlib.Algebra.Group.Center
Cited by
57 results in Mathlib
Foundations
Depth 4 from the axioms · uses no axioms
Assumes
Mul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Submonoid.centralizer · cited by 15Submonoid.centralizerSubsemiring.centralizer · cited by 13Subsemiring.centralizerSet.subset_centralizer_centralizer · cited by 13Set.subset_centralizer_ce…Set.centralizer_centralizer_comm_of_comm · cited by 11Set.centralizer_centraliz…Set.centralizer_subset · cited by 11Set.centralizer_subsetNonUnitalSubsemiring.centralizer · cited by 10NonUnitalSubsemiring.cent…Subsemigroup.centralizer · cited by 10Subsemigroup.centralizerSet.centralizer_univ · cited by 10Set.centralizer_univNonUnitalSubring.centralizer · cited by 10NonUnitalSubring.centrali…Set.center_subset_centralizer · cited by 8Set.center_subset_central…Set.centralizer_eq_top_iff_subset · cited by 8Set.centralizer_eq_top_if…Set.isClosed_centralizer · cited by 4Set.isClosed_centralizerSet.centralizer_centralizer_centralizer · cited by 3Set.centralizer_centraliz…NonUnitalStarAlgebra.adjoin_le_centralizer_centralizer · cited by 2NonUnitalStarAlgebra.adjo…NonUnitalStarSubalgebra.coe_centralizer · cited by 2NonUnitalStarSubalgebra.c…Set · cited by 53352SetSet.ofPred · cited by 6101Set.ofPredSet.centralizerCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement and proof · cited by 53,352
  • Set.ofPredproof · cited by 6,101

Cited by67

Results whose statement or proof uses this declaration.