mul_invOf_cancel_left — Mathlib

English

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

Русский

Пусть A обратима. Тогда A · (A^{-1} · B) = B для любого B.

LaTeX

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

Lean4

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

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