Theorems · Theorem · linear algebra

Matrix.updateCol.congr_simp

∀ {m : Type u_2} {n : Type u_3} {α : Type v} {inst : DecidableEq n} [inst_1 : DecidableEq n] (M M_1 : Matrix m n α),
  M = M_1 →
    ∀ (j j_1 : n),
      j = j_1 →
        ∀ (b b_1 : m → α),
          b = b_1 →
            ∀ (a a_1 : m), a = a_1 → ∀ (a_2 a_3 : n), a_2 = a_3 → M.updateCol j b a a_2 = M_1.updateCol j_1 b_1 a_1 a_3

Defined in: Mathlib.LinearAlgebra.Matrix.RowCol
Cited by: 3 results in Mathlib
Foundations: Depth 15 from the axioms · uses Quot.sound
Assumes: DecidableEq

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Matrixstatement and proof · cited by 4,303
Matrix.updateColstatement and proof · cited by 45

Cited by3

Results whose statement or proof uses this declaration.

Polynomial.resultant_C_mul_rightproof · cited by 5
Algebra.discr_mul_isIntegral_mem_adjoinproof · cited by 1
Matrix.updateCol_subsingletonproof · cited by 0