toQuadraticMap_eq_zero — Mathlib

English

A BilinMap B has zero quadratic map iff it is alternating: B.toQuadraticMap = 0 iff B.IsAlt.

Русский

У билинейного отображения B квадратичное отображение равно нулю тогда и только тогда, когда B - чередующее: B.toQuadraticMap = 0 ⇔ B.IsAlt.

LaTeX

$$$B.toQuadraticMap = 0 \iff B.IsAlt$$$

Lean4

@[simp]
theorem toQuadraticMap_eq_zero {B : BilinMap R M N} : B.toQuadraticMap = 0 ↔ B.IsAlt :=
  QuadraticMap.ext_iff

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