monomial_neg — Mathlib

English

Negation distributes over monomials: monomial n with coefficient -a equals the negation of monomial n with coefficient a.

Русский

Отрицание распадается на мономиал: моно́мие n с коэффициентом -a равно - моному с коэффициентом a.

LaTeX

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

Lean4

@[simp]
theorem monomial_neg (n : ℕ) (a : R) : monomial n (-a) = -monomial n a := by
  rw [eq_neg_iff_add_eq_zero, ← monomial_add, neg_add_cancel, monomial_zero_right]

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