detInvertibleOfRightInverse — Mathlib

English

If there exists a right inverse B with A B = 1, then det(A) is invertible and its inverse is B.det.

Русский

Если существует правый обратный B с A B = 1, то det(A) обратим и inv det(A) = B.det.

LaTeX

$$$(\exists B)(A B = 1) \Rightarrow \text{Invertible}(\det A) \text{ and } invOf(\det A) = B.det$$$

Lean4

/-- `A.det` is invertible if `A` has a right inverse. -/
def detInvertibleOfRightInverse (h : A * B = 1) : Invertible A.det
    where
  invOf := B.det
  mul_invOf_self := by rw [← det_mul, h, det_one]
  invOf_mul_self := by rw [mul_comm, ← det_mul, h, det_one]

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