ite_div — Mathlib

English

For any P, a, b, c with Div, (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_div (a b c : α) : (if P then a else b) / c = if P then a / c else b / c :=
  dite_div ..

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