toMatrix_eq_transpose — Mathlib

English

The matrix of the Pi basis of functions is exactly the transpose of the standard matrix representation.

Русский

Матрица базиса Pi функций равна транспонированной стандартной матричной записи.

LaTeX

$$$((\\Pi\\text{basisFun} \\; R\\; \\iota).toMatrix) = \\text{Matrix.transpose}$$$

Lean4

theorem toMatrix_eq_transpose [Finite ι] :
    ((Pi.basisFun R ι).toMatrix : Matrix ι ι R → Matrix ι ι R) = Matrix.transpose :=
  by
  ext M i j
  rfl

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