mul_ite — Mathlib

English

For any a, b, c in a semiring, a * (if P then b else c) = if P then a * b else a * c.

Русский

Для любых a, b, c в полумножестве: a умножить на (если P тогда b иначе c) равняется (если P тогда a*b иначе a*c).

LaTeX

$$$$a * (\text{if }P\text{ then } b\text{ else } c) = \text{if }P\text{ then } a*b\text{ else } a*c.$$$$

Lean4

@[to_additive]
theorem mul_ite (a b c : α) : (a * if P then b else c) = if P then a * b else a * c :=
  mul_dite ..

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