Theorems · Theorem · linear algebra

Matrix.submatrix_submatrix

∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {l₂ : Type u_10} {o₂ : Type u_11}
  (A : Matrix m n α) (r₁ : l → m) (c₁ : o → n) (r₂ : l₂ → l) (c₂ : o₂ → o),
  (A.submatrix r₁ c₁).submatrix r₂ c₂ = A.submatrix (r₁ ∘ r₂) (c₁ ∘ c₂)

Defined in

Mathlib.LinearAlgebra.Matrix.Defs

Cited by

24 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound