cramer_row_self — Mathlib

English

If b_j = A_j i for all j, then A.cramer b equals the i-th standard basis vector times det A.

Русский

Если b_j = A_{j i} для всех j, то A.cramer b = e_i · det A.

LaTeX

$$$$A.cramer b = \\mathbf{e}_i \\cdot \\det A \\quad\\text{when } b_j = A_{j i} \\text{ for all } j.$$$$

Lean4

theorem cramer_row_self (i : n) (h : ∀ j, b j = A j i) : A.cramer b = Pi.single i A.det :=
  by
  rw [← transpose_transpose A, det_transpose]
  convert cramer_transpose_row_self Aᵀ i
  exact funext h

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