ext_basis — Mathlib

English

Two bilinear forms are equal if they agree on all pairs of basis vectors. If B(b_i, b_j) = F₂(b_i, b_j) for all basis indices i, j, then B = F₂.

Русский

Две билинейные формы равны, если они совпадают на всех парах базисных векторов. Если B(b_i, b_j) = F₂(b_i, b_j) для всех i, j, то B = F₂.

LaTeX

$$$ \\forall i,j,\\ B(b_i,b_j) = F_2(b_i,b_j) \\Rightarrow B = F_2 $$$

Lean4

/-- Two bilinear forms are equal when they are equal on all basis vectors. -/
theorem ext_basis (h : ∀ i j, B (b i) (b j) = F₂ (b i) (b j)) : B = F₂ :=
  b.ext fun i => b.ext fun j => h i j

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