cramer_one — Mathlib

English

Cramer's rule applied to the identity matrix gives the identity map: cramer(I) = I.

Русский

Применение правила Крамера к единичной матрице даёт тожество: cramer(I) = I.

LaTeX

$$$$cramer(1) = 1.$$$$

Lean4

@[simp]
theorem cramer_one : cramer (1 : Matrix n n α) = 1 := by
  ext i j
  convert congr_fun (cramer_row_self (1 : Matrix n n α) (Pi.single i 1) i _) j
  · simp
  · intro j
    rw [Matrix.one_eq_pi_single, Pi.single_comm]

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