Theorems · Theorem · group theory
Commute.refl
∀ {S : Type u_3} [inst : Mul S] (a : S), Commute a aAny element commutes with itself.
- Defined in
- Mathlib.Algebra.Group.Commute.Defs
- Cited by
- 38 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- Mul
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Commutestatement · cited by 639
Cited by38
Results whose statement or proof uses this declaration.
- Commute.geom_sum₂_mulproof · cited by 4
- Commute.geom_sum₂_mul_addproof · cited by 3
- Equiv.Perm.self_mem_cycle_factors_commuteproof · cited by 3
- hasFDerivAt_exp_smul_const_of_mem_ballproof · cited by 3
- CircleDeg1Lift.translationNumber_units_invproof · cited by 2
- hasStrictFDerivAt_exp_smul_const_of_mem_ball'proof · cited by 2
- Commute.pow_pow_selfproof · cited by 2
- ContinuousLinearMap.IsIdempotentElem.isSelfAdjoint_iff_isStarNormalproof · cited by 2
- NormedSpace.exp_nsmulproof · cited by 2
- commutatorElement_selfproof · cited by 1
- Commute.orderOf_dvd_lcm_mulproof · cited by 1
- Equiv.Perm.cycleFactorsFinset_mem_commute'proof · cited by 1