cramer_zero — Mathlib

English

If A is the zero matrix and n is nontrivial, then cramer(0) = 0.

Русский

Если A — нулевая матрица, и n не тривиально, то cramer(0) = 0.

LaTeX

$$$$cramer(0) = 0 \\quad\\text{when } \\text{Nontrivial}(n).$$$$

Lean4

theorem cramer_zero [Nontrivial n] : cramer (0 : Matrix n n α) = 0 :=
  by
  ext i j
  obtain ⟨j', hj'⟩ : ∃ j', j' ≠ j := exists_ne j
  apply det_eq_zero_of_column_eq_zero j'
  intro j''
  simp [updateCol_ne hj']

Похожие утверждения