Theorems · Theorem · linear algebra

Matrix.mul_submatrix_one

∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : Fintype n] [Finite o]
  [inst_2 : NonAssocSemiring α] [inst_3 : DecidableEq o] (e₁ : n ≃ o) (e₂ : l → o) (M : Matrix m n α),
  M * Matrix.submatrix 1 (⇑e₁) e₂ = M.submatrix id (⇑e₁.symm ∘ e₂)

Defined in

Mathlib.Data.Matrix.Mul

Cited by

1 results in Mathlib

Foundations

Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeFiniteNonAssocSemiringDecidableEq