Theorems · Theorem · linear algebra

Matrix.updateCol_submatrix_equiv

∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : DecidableEq o]
  [inst_1 : DecidableEq n] (A : Matrix m n α) (j : o) (c : l → α) (e : l ≃ m) (f : o ≃ n),
  (A.submatrix ⇑e ⇑f).updateCol j c = (A.updateCol (f j) fun i => c (e.symm i)).submatrix ⇑e ⇑f

Defined in

Mathlib.LinearAlgebra.Matrix.RowCol

Cited by

3 results in Mathlib

Foundations

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

Assumes

DecidableEqDecidableEq