cramer_transpose_row_self — Mathlib

English

If b_j = A_j i for all j, then A.cramer b = e_i · det(A); i.e., the Cramer's map selects the i-th basis vector scaled by det(A).

Русский

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

LaTeX

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

Lean4

theorem cramer_transpose_row_self (i : n) : Aᵀ.cramer (A i) = Pi.single i A.det :=
  by
  ext j
  rw [cramer_apply, Pi.single_apply]
  split_ifs with h
  · -- i = j: this entry should be `A.det`

    subst h
    simp only [updateCol_transpose, det_transpose, updateRow_eq_self]
  · -- i ≠ j: this entry should be 0

    rw [updateCol_transpose, det_transpose]
    apply det_zero_of_row_eq h
    rw [updateRow_self, updateRow_ne (Ne.symm h)]

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