inv — Mathlib

English

The inverse of a square matrix A (when invertible) equals det(A)^{-1} times adjugate(A).

Русский

Обратная матрица A равна det(A)^{-1} умноженной на приспособление (адьюгат) A, если A обратима.

LaTeX

$$$A^{-1} = \\det(A)^{-1} \\operatorname{adj}(A)$$$

Lean4

/-- The inverse of a square matrix, when it is invertible (and zero otherwise). -/
noncomputable instance inv : Inv (Matrix n n α) :=
  ⟨fun A => Ring.inverse A.det • A.adjugate⟩

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