div_ite — Mathlib

English

For any P, a, b, c with Div, a / (if P then b else c) = if P then a / b else a / c.

Русский

Для любых P, 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 div_ite (a b c : α) : (a / if P then b else c) = if P then a / b else a / c :=
  div_dite ..

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