mul_adjugate — Mathlib

English

Let A be an n-by-n matrix over a commutative ring. Then the product of A with its adjugate equals the determinant of A times the identity matrix: A · adj(A) = det(A) I_n.

Русский

Пусть A — матрица размера n×n над коммутативным кольцом. Тогда произведение A на adj(A) равно det(A) умножить на единичную матрицу: A · adj(A) = det(A) I_n.

LaTeX

$$$A \cdot \operatorname{adj}(A) = \det(A) \; I_n$$$

Lean4

theorem mul_adjugate (A : Matrix n n α) : A * adjugate A = A.det • (1 : Matrix n n α) :=
  by
  ext i j
  rw [mul_apply, Pi.smul_apply, Pi.smul_apply, one_apply, smul_eq_mul, mul_boole]
  simp [mul_adjugate_apply, sum_cramer_apply, cramer_transpose_row_self, Pi.single_apply, eq_comm]

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