fromMatrix_apply_single_one — Mathlib

English

For any index j, applying PiToModule.fromMatrix to the standard basis vector e_j in ι → R yields the sum ∑_i A_{i j} b_i.

Русский

Для любого индекса j применение PiToModule.fromMatrix к стандартному базисному вектору e_j даёт сумму ∑_i A_{i j} b_i.

LaTeX

$$PiToModule.fromMatrix R b A (e_j) = ∑_i A_{i j} b_i$$

Lean4

theorem fromMatrix_apply_single_one [DecidableEq ι] (A : Matrix ι ι R) (j : ι) :
    PiToModule.fromMatrix R b A (Pi.single j 1) = ∑ i : ι, A i j • b i :=
  by
  rw [PiToModule.fromMatrix_apply, Fintype.linearCombination_apply, Matrix.mulVec_single]
  simp_rw [MulOpposite.op_one, one_smul, col_apply]

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