adjugate_one — Mathlib

English

If A is diagonal with diagonal entries v, then adjugate(A) is diagonal with i-th diagonal entry ∏_{j≠i} v_j.

Русский

Если A диагональная с диагональными элементами v, то adjugate(A) также диагональная и её i-й диагональный элемент равен произведению по j≠i из v_j.

LaTeX

$$$\operatorname{adj}(\operatorname{diag}(v)) = \operatorname{diag}\left( \prod_{j \in \mathrm{univ} \setminus \{i\}} v_j \right)_{i}$$$

Lean4

@[simp]
theorem adjugate_one : adjugate (1 : Matrix n n α) = 1 := by
  ext
  simp [adjugate_def, Matrix.one_apply, Pi.single_apply, eq_comm]

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