unitOfDetInvertible_eq_nonsingInvUnit

English

If [Invertible det(A)], then unitOfDetInvertible A equals nonsingInvUnit A (isUnit_of_invertible).

Русский

Если det(A) обратим, то unitOfDetInvertible A равен nonsingInvUnit A (isUnit_of_invertible).

LaTeX

$$$\text{unitOfDetInvertible } A = \text{ nonsingInvUnit } A (\text{isUnit_of_invertible } _)$. $$

Lean4

theorem unitOfDetInvertible_eq_nonsingInvUnit [Invertible A.det] :
    unitOfDetInvertible A = nonsingInvUnit A (isUnit_of_invertible _) :=
  by
  ext
  rfl

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