associated_toQuadraticMap — Mathlib

English

If B1 is symmetric, then its associatedHom equals B1.

Русский

Если B1 симметрично, то associatedHom B1.toQuadraticMap совпадает с B1.

LaTeX

$$$ \text{associated_left_inverse} \; (h:\forall x,y, B_1 x y = B_1 y x) : \; associatedHom S B_1.toQuadraticMap = B_1 $$$

Lean4

theorem associated_toQuadraticMap (B : BilinMap R M N) (x y : M) :
    associatedHom S B.toQuadraticMap x y = ⅟(2 : Module.End R N) • (B x y + B y x) :=
  by
  simp only [associated_apply, BilinMap.toQuadraticMap_apply, map_add, LinearMap.add_apply, Module.End.smul_def,
    map_sub]
  abel_nf

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