mul_adjugate_apply — Mathlib

English

For i,k,j, A_{i k} · adjugate A_{k j} equals the j-th component of cramer Aᵀ applied to the unit vector with a 1 in position k and value A_{i k}. In symbols: A_{i k} · adjugate A_{k j} = cramer(Aᵀ, e_k A_{i k})_j.

Русский

Для i,k,j: A_{i k} · adjugate A_{k j} = cramer(Aᵀ, e_k A_{i k})_j.

LaTeX

$$$$A_{i k} \\cdot \\operatorname{adjugate}(A)_{k j} = \\bigl( \\mathrm{cramer}(A^{\\top}, \\mathbf{e}_k\\, A_{i k}) \\bigr)_j.$$$$

Lean4

theorem mul_adjugate_apply (A : Matrix n n α) (i j k) : A i k * adjugate A k j = cramer Aᵀ (Pi.single k (A i k)) j := by
  rw [← smul_eq_mul, adjugate, of_apply, ← Pi.smul_apply, ← LinearMap.map_smul, ← Pi.single_smul', smul_eq_mul, mul_one]

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