isUnit_toMatrix — Mathlib

English

A pair of matrices associated with two affine bases multiplies to the identity; this shows a form of basis compatibility.

Русский

Пара матриц, связанных с двумя аффинными базисами, даёт тождественную матрицу; демонстрирует совместимость баз.

LaTeX

$$$b.toMatrix b_2 \\;\\text{and}\\; b_2.toMatrix b \\Rightarrow \\text{identity}$$$

Lean4

theorem isUnit_toMatrix : IsUnit (b.toMatrix b₂) :=
  ⟨{  val := b.toMatrix b₂
      inv := b₂.toMatrix b
      val_inv := b.toMatrix_mul_toMatrix b₂
      inv_val := b₂.toMatrix_mul_toMatrix b }, rfl⟩

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