mulSingle_mul — Mathlib

English

For all i, x, y in f i, we have mulSingle i (x * y) = mulSingle i x * mulSingle i y.

Русский

Пусть для всех i x, y ∈ f i, тогда mulSingle i (x · y) = mulSingle i x · mulSingle i y.

LaTeX

$$$ \mathrm{mulSingle} (i) (x * y) = \mathrm{mulSingle} (i) x * \mathrm{mulSingle} (i) y $$$

Lean4

@[to_additive]
theorem mulSingle_mul [∀ i, MulOneClass <| f i] (i : I) (x y : f i) :
    mulSingle i (x * y) = mulSingle i x * mulSingle i y :=
  (MonoidHom.mulSingle f i).map_mul x y

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