toBilin'_single — Mathlib

English

Taking basis vectors yields the corresponding matrix entry: toBilin' M (Pi.single i 1) (Pi.single j 1) = M_{ij}.

Русский

При взятии базисных векторов получаем соответствующую матричную компоненту: toBilin' M (Pi.single i 1) (Pi.single j 1) = M_{ij}.

LaTeX

$$$\text{toBilin'}\_single(M,i,j) = M_{ij}$$$

Lean4

@[simp]
theorem toBilin'_single (M : Matrix n n R₁) (i j : n) : Matrix.toBilin' M (Pi.single i 1) (Pi.single j 1) = M i j := by
  simp [Matrix.toBilin'_apply, Pi.single_apply]

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