Theorems · Theorem · linear algebra

Matrix.one_submatrix_mul

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

Defined in

Mathlib.Data.Matrix.Mul

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeFiniteNonAssocSemiringDecidableEq