toMatrix_toPEquiv_mul — Mathlib

English

For finite m, m ≃ n, and M ∈ M_{m×n}(α), the product M * f.toPEquiv.toMatrix equals M.submatrix id f.symm.

Русский

Для конечного множества m и биекции f: m ≃ n, для M ∈ M_{m×n}(α): M * f.toPEquiv.toMatrix = M.submatrix id f.symm.

LaTeX

$$$ M * f.toPEquiv.toMatrix = M_{submatrix id}^{f.symm} $$$

Lean4

theorem toMatrix_toPEquiv_mul [Fintype m] [DecidableEq m] [NonAssocSemiring α] (f : l ≃ m) (M : Matrix m n α) :
    f.toPEquiv.toMatrix * M = M.submatrix f id := by
  ext i j
  rw [toMatrix_mul_apply, Equiv.toPEquiv_apply, submatrix_apply, id]

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