coeFn_neg — Mathlib

English

The underlying function of the negation of a quadratic map is the negation of the underlying function: (−Q)(x) = −(Q(x)).

Русский

Функция, лежащая в основе отрицания квадратичной карты, равна отрицанию функции квадратичной карты: (−Q)(x) = −Q(x).

LaTeX

$$$ (\\text{coeFn})((-Q))(x) = - Q(x) $ for all x.$$

Lean4

@[simp, norm_cast]
theorem coeFn_neg (Q : QuadraticMap R M N) : ⇑(-Q) = -Q :=
  rfl

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