mul_mul — Mathlib

English

If a1 is associated with b1 and a2 is associated with b2, then a1*a2 is associated with b1*b2; multiplication respects association.

Русский

Если a1 ассоциировано с b1 и a2 ассоциировано с b2, то a1*a2 ассоциировано с b1*b2; умножение сохраняет ассоциацию.

LaTeX

$$$ [CommMonoid M] {a₁ a₂ b₁ b₂ : M} (h₁ : a₁ ~ᵤ b₁) (h₂ : a₂ ~ᵤ b₂) : a₁ * a₂ ~ᵤ b₁ * b₂ $$$

Lean4

theorem mul_mul [CommMonoid M] {a₁ a₂ b₁ b₂ : M} (h₁ : a₁ ~ᵤ b₁) (h₂ : a₂ ~ᵤ b₂) : a₁ * a₂ ~ᵤ b₁ * b₂ :=
  (h₁.mul_right _).trans (h₂.mul_left _)

Похожие утверждения