toQuadraticMapAddMonoidHom — Mathlib

English

The negation of a BilinMap scales under toQuadraticMap: (-B).toQuadraticMap = -B.toQuadraticMap.

Русский

При отрицании билинейного отображения квадратичное отображение сменяет знак: (-B).toQuadraticMap = -B.toQuadraticMap.

LaTeX

$$$(-B).toQuadraticMap = -B.toQuadraticMap$$$

Lean4

/-- `LinearMap.BilinMap.toQuadraticMap` as an additive homomorphism -/
@[simps]
def toQuadraticMapAddMonoidHom : (BilinMap R M N) →+ QuadraticMap R M N
    where
  toFun := toQuadraticMap
  map_zero' := toQuadraticMap_zero _ _
  map_add' := toQuadraticMap_add

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