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