invOf_eq — Mathlib

English

A variant stating inv(A) equals det(A)^{-1} times adj(A) under the appropriate invertibility assumptions.

Русский

Вариант утверждает inv(A) = det(A)^{-1} adj(A) при соответствующих предпосылках обратимости.

LaTeX

$$$\text{invOf}(A) = \det(A)^{-1} \cdot \operatorname{adj}(A)$ under invertibility assumptions$$

Lean4

theorem invOf_eq [Invertible A.det] [Invertible A] : ⅟A = ⅟A.det • A.adjugate :=
  by
  letI := invertibleOfDetInvertible A
  convert (rfl : ⅟A = _)

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