Mathlib Map

Theorems · Theorem · group theory

Commute.symm

∀ {S : Type u_3} [inst : Mul S] {a b : S}, Commute a b → Commute b a

If a commutes with b, then b commutes with a.

Defined in
Mathlib.Algebra.Group.Commute.Defs
Cited by
79 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
Mul
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Polynomial.map_mul · cited by 90Polynomial.map_mulNat.commute_cast · cited by 13Nat.commute_castCommute.add_pow · cited by 12Commute.add_powSet.centralizer_univ · cited by 10Set.centralizer_univCommute.pow_left · cited by 9Commute.pow_leftSet.center_subset_centralizer · cited by 8Set.center_subset_central…Commute.isNilpotent_mul_left · cited by 7Commute.isNilpotent_mul_l…Matrix.center_eq_scalar_image · cited by 6Matrix.center_eq_scalar_i…Int.commute_cast · cited by 5Int.commute_castCommute.symm_iff · cited by 5Commute.symm_iffCommute.div_mul_div_comm · cited by 5Commute.div_mul_div_commIsLeftRegular.right_of_commute · cited by 4IsLeftRegular.right_of_co…Commute.pow_dvd_pow_of_sub_pow_eq_zero · cited by 3Commute.pow_dvd_pow_of_su…Commute.geom_sum₂_mul_add · cited by 3Commute.geom_sum₂_mul_addIsIdempotentElem.mul_of_commute · cited by 3IsIdempotentElem.mul_of_c…Commute · cited by 639CommuteCommute.symmCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Commutestatement and proof · cited by 639

Cited by79

Results whose statement or proof uses this declaration.