English
For any P, a, b, c in a semiring, (if P then a else b) * c = if P then a * c else b * c.
Русский
Для любых P, a, b, c в полугруппе: (если P то a иначе b) умножить на c равно (если P тогда a*c иначе b*c).
LaTeX
$$$$ (\text{if }P\text{ then } a\text{ else } b) * c = \text{if }P\text{ then } a*c\text{ else } b*c. $$$$
Lean4
@[to_additive]
theorem ite_mul (a b c : α) : (if P then a else b) * c = if P then a * c else b * c :=
dite_mul ..
-- We make `mul_ite` and `ite_mul` simp lemmas, but not `add_ite` or `ite_add`.
-- The problem we're trying to avoid is dealing with sums of the form `∑ x ∈ s, (f x + ite P 1 0)`,
-- in which `add_ite` followed by `sum_ite` would needlessly slice up
-- the `f x` terms according to whether `P` holds at `x`.
-- There doesn't appear to be a corresponding difficulty so far with `mul_ite` and `ite_mul`.
