square_of_invertible — Mathlib

English

If there exist rectangular matrices M and N over a nontrivial commutative semiring R such that MN = NM = 1, then the corresponding ranks are equal; in particular, R satisfies the invariant basis number.

Русский

Если существуют матрицы M и N над не тривиальным коммутативным полем R такие, что MN = NM = 1, то соответствующие размерности равны; следовательно, R удовлетворяет неизмменяемый базис по размерности (IBN).

LaTeX

$$$\exists M,N \ (M:N)\text{ и }(N:M)\text{ с } M N = N M = I \Rightarrow \lvert n \rvert = \lvert m \rvert.$$$

Lean4

theorem square_of_invertible (M : Matrix n m R) (N : Matrix m n R) (h : M * N = 1) (h' : N * M = 1) :
    Fintype.card n = Fintype.card m :=
  card_eq_of_linearEquiv R (Matrix.toLinearEquivRight'OfInv h' h)

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