transpose_toMatrix_toPEquiv_apply

English

For finite m,n with additive commutative semiring α, and e: m ≃ n, M ∈ M_{m×n}(α), the product M.submatrix id e · Mᵀ.submatrix e id equals M · Mᵀ.

Русский

Для конечных множеств m,n и M ∈ M_{m×n}(α) верно M.submatrix id e · Mᵀ.submatrix e id = M · Mᵀ.

LaTeX

$$$ M_{sub}^{id,e} \\cdot M^{\\top}_{sub}^{e,id} = M \\cdot M^{\\top} $$$

Lean4

@[simp]
theorem transpose_toMatrix_toPEquiv_apply [DecidableEq m] [DecidableEq n] [Zero α] [One α] (f : m ≃ n) (j) :
    f.toPEquiv.toMatrixᵀ j = Pi.single (f.symm j) (1 : α) :=
  by
  ext
  simp [toMatrix_apply, Pi.single_apply, eq_comm, ← Equiv.apply_eq_iff_eq_symm_apply]

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