Mathlib Map

Theorems · Theorem · group theory

Set.centralizer_subset

∀ {M : Type u_1} {S T : Set M} [inst : Mul M], S ⊆ T → T.centralizer ⊆ S.centralizer
Defined in
Mathlib.Algebra.Group.Center
Cited by
11 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.

Submonoid.centralizer_le · cited by 1Submonoid.centralizer_leNonUnitalStarSubalgebra.centralizer_le · cited by 0NonUnitalStarSubalgebra.c…NonUnitalSubsemiring.centralizer_le · cited by 0NonUnitalSubsemiring.cent…NonUnitalSubalgebra.centralizer_le · cited by 0NonUnitalSubalgebra.centr…StarSubalgebra.centralizer_le · cited by 0StarSubalgebra.centralize…commutator_centralizer_commutator_le_center · cited by 0commutator_centralizer_co…Subsemigroup.centralizer_le · cited by 0Subsemigroup.centralizer_…NonUnitalSubring.centralizer_le · cited by 0NonUnitalSubring.centrali…Subring.centralizer_le · cited by 0Subring.centralizer_leSubalgebra.centralizer_le · cited by 0Subalgebra.centralizer_leSubsemiring.centralizer_le · cited by 0Subsemiring.centralizer_leSet · cited by 53352SetSet.centralizer · cited by 57Set.centralizerSet.centralizer_subsetCITED 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 by11

Results whose statement or proof uses this declaration.