map_zero

Mathlib.LinearAlgebra.QuadraticForm.Basic

URI: https://scilib.ai/kg/mathlib#QuadraticMap.map_zero

English

A quadratic map sends the zero vector to zero: Q(0) = 0.

Русский

Квадратичная карта отправляет нуль в нуль: Q(0) = 0.

LaTeX

$$Q(0) = 0$$

Lean4

protected theorem map_zero : Q 0 = 0 := by rw [← @zero_smul R _ _ _ _ (0 : M), Q.map_smul, zero_mul, zero_smul]

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

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

Разделы

Аффилиация

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