elim_div_div — Mathlib

English

For any i, Sum.elim (a / a') (b / b') = Sum.elim a b / Sum.elim a' b' when γ is a Div monoid.

Русский

Для любых функций a, a' из α→γ и b, b' из β→γ выполняется Sum.elim (a / a') (b / b') = Sum.elim a b / Sum.elim a' b'.

LaTeX

$$$ \mathrm{Sum.elim} (a / a') (b / b') = \mathrm{Sum.elim} a b / \mathrm{Sum.elim} a' b' $$$

Lean4

@[to_additive]
theorem elim_div_div [Div γ] : Sum.elim (a / a') (b / b') = Sum.elim a b / Sum.elim a' b' :=
  by
  ext x
  cases x <;> rfl

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