Theorems · Definition · group theory
AddSubsemigroup.centralizer
{M : Type u_1} → Set M → [inst : AddSemigroup M] → AddSubsemigroup MThe centralizer of a subset of an additive semigroup.
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
- Assumes
- AddSemigroup
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
- AddSubsemigroupstatement · cited by 262
- AddSemigroupstatement and proof · cited by 136
- Set.addCentralizerproof · cited by 20
- Set.add_mem_addCentralizerproof · cited by 1
Cited by9
Results whose statement or proof uses this declaration.
- AddSubsemigroup.closure_le_centralizer_centralizerstatement · cited by 1
- AddSubsemigroup.isAddCommutative_closureproof · cited by 0
- AddSubsemigroup.centralizer_eq_top_iff_subsetstatement · cited by 0
- AddSubsemigroup.centralizer_lestatement · cited by 0
- AddSubsemigroup.centralizer_univstatement · cited by 0
- AddSubmonoid.centralizer_toAddSubsemigroupstatement · cited by 0
- AddSubsemigroup.mem_centralizer_iffstatement · cited by 0
- AddSubsemigroup.coe_centralizerstatement · cited by 0
- AddSubsemigroup.center_le_centralizerstatement · cited by 0