toQuadraticMap_zero

Mathlib.LinearAlgebra.QuadraticForm.Basic

URI: https://scilib.ai/kg/mathlib#LinearMap.BilinMap.toQuadraticMap_zero

English

There is an additive monoid hom from BilinMap to QuadraticMap sending B to toQuadraticMap B.

Русский

Существует гомоморфизм аддитивного моноида BilinMap → QuadraticMap, отправляющий B в toQuadraticMap B.

LaTeX

$$$toQuadraticMapAddMonoidHom : BilinMap \to QuadraticMap$ is an additive monoid hom.$$

Lean4

@[simp]
theorem toQuadraticMap_zero : (0 : BilinMap R M N).toQuadraticMap = 0 :=
  rfl

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

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

Разделы

Аффилиация

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