Theorems · Definition · group theory
Subsemigroup.centralizer
{M : Type u_1} → Set M → [inst : Semigroup M] → Subsemigroup MThe centralizer of a subset of a semigroup M.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
- Assumes
- Semigroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- Subsemigroupstatement · cited by 323
- Semigroupstatement and proof · cited by 202
- Set.centralizerproof · cited by 57
- Set.mul_mem_centralizerproof · cited by 2
Cited by11
Results whose statement or proof uses this declaration.
- NonUnitalSubsemiring.centralizerproof · cited by 10
- Subsemigroup.closure_le_centralizer_centralizerstatement · cited by 1
- NonUnitalSubsemiring.centralizer_toSubsemigroupstatement · cited by 0
- Subsemigroup.coe_centralizerstatement · cited by 0
- Subsemigroup.center_le_centralizerstatement · cited by 0
- Subsemigroup.isMulCommutative_closureproof · cited by 0
- Subsemigroup.centralizer_eq_top_iff_subsetstatement · cited by 0
- Subsemigroup.centralizer_lestatement · cited by 0
- Subsemigroup.centralizer_univstatement · cited by 0
- Subsemigroup.mem_centralizer_iffstatement · cited by 0
- Submonoid.centralizer_toSubsemigroupstatement · cited by 0