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)