detInvertibleOfLeftInverse — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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