monomial_sub — Mathlib

English

The monomial distributes over subtraction: monomial n (a − b) = monomial n a − monomial n b.

Русский

Мономиал распределяется по вычитанию: мономиал n (a − b) = мономиал n a − мономиал n b.

LaTeX

$$$\mathrm{monomial}(n, a - b) = \mathrm{monomial}(n, a) - \mathrm{monomial}(n, b)$$$

Lean4

theorem monomial_sub (n : ℕ) : monomial n (a - b) = monomial n a - monomial n b := by
  rw [sub_eq_add_neg, monomial_add, monomial_neg, sub_eq_add_neg]

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