instZero

Mathlib.LinearAlgebra.AffineSpace.AffineMap

URI: https://scilib.ai/kg/mathlib#AffineMap.instZero

English

There is a natural negation on affine maps: -f is defined by (-f)(p) = -f(p) and (-f).linear = -f.linear.

Русский

Существует естественное отрицание аффинного отображения: (-f)(p) = -f(p) и (-f).linear = -f.linear.

LaTeX

$$$(-f)(p) = -f(p)\quad\text{and}\quad (-f)_{\mathrm{linear}} = - f_{\mathrm{linear}}$$$

Lean4

instance : Zero (P1 →ᵃ[k] V2) where zero := ⟨0, 0, fun _ _ => (zero_vadd _ _).symm⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru