elim_mul_mul — Mathlib

English

For any i, the Sum.elim distributes multiplication pointwise: Sum.elim (a * a') (b * b') = Sum.elim a b * Sum.elim a' b'.

Русский

Для любых функций a, a' из α→γ и b, b' из β→γ имеем: Sum.elim (a * a') (b * b') = Sum.elim a b * Sum.elim a' b'.

LaTeX

$$$ \mathrm{Sum.elim} (a * a') (b * b') = \mathrm{Sum.elim} a b * \mathrm{Sum.elim} a' b' $$$

Lean4

@[to_additive]
theorem elim_mul_mul [Mul γ] : Sum.elim (a * a') (b * b') = Sum.elim a b * Sum.elim a' b' :=
  by
  ext x
  cases x <;> rfl

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