Mathlib Map

Theorems · Theorem · group theory

Set.subset_centralizer_centralizer

∀ {M : Type u_1} {S : Set M} [inst : Mul M], S ⊆ S.centralizer.centralizer
Defined in
Mathlib.Algebra.Group.Center
Cited by
13 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
Mul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

NonUnitalAlgebra.adjoin_le_centralizer_centralizer · cited by 4NonUnitalAlgebra.adjoin_l…Algebra.adjoin_le_centralizer_centralizer · cited by 3Algebra.adjoin_le_central…Set.centralizer_centralizer_centralizer · cited by 3Set.centralizer_centraliz…Subgroup.closure_le_centralizer_centralizer · cited by 2Subgroup.closure_le_centr…NonUnitalSubring.closure_le_centralizer_centralizer · cited by 1NonUnitalSubring.closure_…Subring.closure_le_centralizer_centralizer · cited by 1Subring.closure_le_centra…Subsemiring.closure_le_centralizer_centralizer · cited by 1Subsemiring.closure_le_ce…NonUnitalSubsemiring.closure_le_centralizer_centralizer · cited by 1NonUnitalSubsemiring.clos…Submonoid.closure_le_centralizer_centralizer · cited by 1Submonoid.closure_le_cent…Subsemigroup.closure_le_centralizer_centralizer · cited by 1Subsemigroup.closure_le_c…Submonoid.le_centralizer_centralizer · cited by 0Submonoid.le_centralizer_…Subsemiring.le_centralizer_centralizer · cited by 0Subsemiring.le_centralize…Subalgebra.le_centralizer_centralizer · cited by 0Subalgebra.le_centralizer…Set · cited by 53352SetSet.centralizer · cited by 57Set.centralizerSet.subset_centralizer_centra…CITED 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.centralizerstatement and proof · cited by 57

Cited by13

Results whose statement or proof uses this declaration.