Theorems · Theorem · linear algebra

Matrix.det_eq_of_forall_row_eq_smul_add_pred_aux

∀ {R : Type v} [inst : CommRing R] {n : ℕ} (k : Fin (n + 1)) (c : Fin n → R),
  (∀ (i : Fin n), k < i.succ → c i = 0) →
    ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
      (∀ (j : Fin n.succ), M 0 j = N 0 j) →
        (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det

Defined in

Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRing