ite_div_ite — Mathlib

English

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

Русский

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

LaTeX

$$$$\dfrac{\text{if }P\text{ then } a\text{ else } b}{\text{if }P\ then c\text{ else } d} = \text{if }P\ then a / c \text{ else } b / d.$$$$

Lean4

@[to_additive]
theorem ite_div_ite (a b c d : α) : ((if P then a else b) / if P then c else d) = if P then a / c else b / d :=
  dite_div_dite ..

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