Theorems · Theorem · group theory
Commute.one_right
∀ {M : Type u_2} [inst : MulOneClass M] (a : M), Commute a 1- Defined in
- Mathlib.Algebra.Group.Commute.Defs
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
- Assumes
- MulOneClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MulOneClassstatement and proof · cited by 1,018
- Commutestatement · cited by 639
- SemiconjBy.one_rightproof · cited by 3
Cited by22
Results whose statement or proof uses this declaration.
- geom_sum_mulproof · cited by 15
- sq_eq_one_iffproof · cited by 14
- mul_self_eq_one_iffproof · cited by 7
- fwdDiff_iter_eq_sum_shiftproof · cited by 5
- MvPowerSeries.commute_Xproof · cited by 4
- neg_one_pow_expChar_powproof · cited by 2
- MonoidHom.commute_inl_inrproof · cited by 2
- sub_one_dvd_pow_sub_oneproof · cited by 2
- geom_sum_mul_addproof · cited by 2
- Commute.one_div_add_one_divproof · cited by 2
- IsUltrametricDist.isUltrametricDist_of_forall_norm_natCast_le_oneproof · cited by 1
- shift_eq_sum_fwdDiff_iterproof · cited by 1