invOf_mul_cancel_left — Mathlib

English

If A is invertible, then ⅟A · (A · B) = B for any B of compatible size; i.e., left-cancellation using the inverse of A.

Русский

Пусть A обратима. Тогда ⅟A · (A · B) = B для любого B подходящего размера.

LaTeX

$$$(A)^{-1}\,(A\,B) = B \quad(\text{with }A\text{ invertible})$$$

Lean4

/-- A copy of `invOf_mul_cancel_left` for rectangular matrices. -/
protected theorem invOf_mul_cancel_left (A : Matrix n n α) (B : Matrix n m α) [Invertible A] : ⅟A * (A * B) = B := by
  rw [← Matrix.mul_assoc, invOf_mul_self, Matrix.one_mul]

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