indexEquivOfInv — Mathlib

English

If M and M' are inverse matrices, there is an equivalence of index types m ≃ n.

Русский

Если M и M' — обратные матрицы, существует эквивалентность множеств индексов m ≃ n.

LaTeX

$$def indexEquivOfInv {M : Matrix m n A} {M' : Matrix n m A} (hMM' : M * M' = 1) (hM'M : M' * M = 1) : m ≃ n$$

Lean4

/-- If `M` and `M'` are each other's inverse matrices, they are square matrices up to
equivalence of types. -/
def indexEquivOfInv [Nontrivial A] [DecidableEq m] [DecidableEq n] {M : Matrix m n A} {M' : Matrix n m A}
    (hMM' : M * M' = 1) (hM'M : M' * M = 1) : m ≃ n :=
  equivOfPiLEquivPi (toLin'OfInv hMM' hM'M)

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