English
Composing two left multiplications by y and then x yields left multiplication by x y. Equivalently, (x ·) ∘ (y ·) = (x y ·).
Русский
_COMпозиция двух левосторонних умножений на y затем на x равна левому умножению на x y_.
LaTeX
$$$ (x \cdot) \circ (y \cdot) = (xy) \cdot $$$
Lean4
/-- Composing two multiplications on the left by `y` then `x`
is equal to a multiplication on the left by `x * y`.
-/
@[to_additive (attr := simp) /-- Composing two additions on the left by `y` then `x`
is equal to an addition on the left by `x + y`. -/
]
theorem comp_mul_left (x y : α) : (x * ·) ∘ (y * ·) = (x * y * ·) :=
by
ext z
simp [mul_assoc]
