Theorems · Inductive type · group theory
IsMulCentral
{M : Type u_1} → [Mul M] → M → PropConditions for an element to be multiplicatively central
- Defined in
- Mathlib.Algebra.Group.Center
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- Mul
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by17
Results whose statement or proof uses this declaration.
- Set.centerproof · cited by 49
- IsMulCentral.commstatement and proof · cited by 26
- IsMulCentral.right_assocstatement and proof · cited by 9
- IsMulCentral.left_assocstatement and proof · cited by 7
- Set.mem_center_iffstatement · cited by 2
- isMulCentral_iffstatement and proof · cited by 2
- IsMulCentral.mid_assocstatement and proof · cited by 1
- CompleteOrthogonalIdempotents.of_ker_isNilpotent_of_isMulCentralstatement and proof · cited by 1
- IsMulCentral.right_commstatement and proof · cited by 1
- Subsemigroup.mem_corner_iff_mem_range_mul_leftstatement and proof · cited by 1
- Subsemigroup.mem_corner_iff_mul_leftstatement and proof · cited by 1
- IsMulCentral.casesOnstatement and proof · cited by 1