Theorems · Theorem · group theory
mul_mul_mul_comm
∀ {G : Type u_3} [inst : CommSemigroup G] (a b c d : G), a * b * (c * d) = a * c * (b * d)- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 65 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses propext
- Assumes
- CommSemigroup
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.
- mul_assocproof · cited by 1,667
- mul_left_commproof · cited by 184
- CommSemigroupstatement and proof · cited by 62
Cited by65
Results whose statement or proof uses this declaration.
- Multiset.prod_map_mulproof · cited by 16
- Complex.cos_addproof · cited by 11
- Matrix.det_fromBlocks_zero₂₁proof · cited by 10
- Height.mulHeight_smul_eq_mulHeightproof · cited by 6
- IsAlgebraic.mulproof · cited by 5
- gaussSum_mul_gaussSum_eq_cardproof · cited by 4
- Asymptotics.IsBigOWith.smulproof · cited by 3
- Height.mulHeight_eval_leproof · cited by 3
- Height.mulHeight_fun_mul_eqproof · cited by 3
- Polynomial.irreducible_of_monicproof · cited by 3
- Finset.sum_sq_le_sum_mul_sum_of_sq_le_mulproof · cited by 3
- MonoidWithZeroHom.mem_valueGroup_iff_of_commproof · cited by 3