inv_mul — Mathlib

English

Multiplying the inverse matrix with the matrix yields the identity: t.inv.toMatrix * t.toMatrix = 1.

Русский

Умножение обратной матрицы на матрицу даёт единичную матрицу: t.inv.toMatrix * t.toMatrix = 1.

LaTeX

$$$t.inv.toMatrix \\cdot t.toMatrix = 1$$$

Lean4

theorem inv_mul (t : TransvectionStruct n R) : t.inv.toMatrix * t.toMatrix = 1 :=
  by
  rcases t with ⟨_, _, t_hij⟩
  simp [toMatrix, transvection_mul_transvection_same, t_hij]

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