Theorems · Theorem · linear algebra

Matrix.submatrix_mul

∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : Fintype n] [inst_1 : Fintype o]
  [inst_2 : Mul α] [inst_3 : AddCommMonoid α] {p : Type u_10} {q : Type u_11} (M : Matrix m n α) (N : Matrix n p α)
  (e₁ : l → m) (e₂ : o → n) (e₃ : q → p),
  Function.Bijective e₂ → (M * N).submatrix e₁ e₃ = M.submatrix e₁ e₂ * N.submatrix e₂ e₃

Defined in

Mathlib.Data.Matrix.Mul

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeFintypeMulAddCommMonoid