toBilin_apply — Mathlib

English

For any quadratic map Q, basis bm, and indices i,j, the bilinear map toBilin evaluated at bm i, bm j equals Q(bm i) if i=j, polar(Q)(bm i, bm j) if i<j, and 0 if i>j.

Русский

Для любого квадратичного отображения Q, базы bm и индексов i,j билинейная карта toBilin(Q,bm) при вводе bm_i, bm_j дает Q(bm_i) если i=j; polar(Q)(bm_i,bm_j) если i<j; и 0 если i>j.

LaTeX

$$$Q.toBilin\\, bm\\ (bm_i)(bm_j) = \\begin{cases} Q(bm_i), & i=j, \\\\ polar(Q)(bm_i, bm_j), & ij. \\end{cases}$$$

Lean4

theorem toBilin_apply (Q : QuadraticMap R M N) (bm : Basis ι R M) (i j : ι) :
    Q.toBilin bm (bm i) (bm j) = if i = j then Q (bm i) else if i < j then polar Q (bm i) (bm j) else 0 := by
  simp [toBilin]

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