feat: port LinearAlgebra.Matrix.InvariantBasisNumber (#3697)

Mathlib.lean

@@ -1427,6 +1427,7 @@ import Mathlib.LinearAlgebra.Matrix.Block
 import Mathlib.LinearAlgebra.Matrix.Circulant
 import Mathlib.LinearAlgebra.Matrix.Determinant
 import Mathlib.LinearAlgebra.Matrix.DotProduct
+import Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
 import Mathlib.LinearAlgebra.Matrix.MvPolynomial
 import Mathlib.LinearAlgebra.Matrix.Nondegenerate
 import Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Mathlib/LinearAlgebra/Matrix/InvariantBasisNumber.lean

@@ -0,0 +1,29 @@
+/-
+Copyright (c) 2022 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+
+! This file was ported from Lean 3 source module linear_algebra.matrix.invariant_basis_number
+! leanprover-community/mathlib commit 843240b048bbb19942c581fd64caecbbe96337be
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.LinearAlgebra.Matrix.ToLin
+import Mathlib.LinearAlgebra.InvariantBasisNumber
+
+/-!
+# Invertible matrices over a ring with invariant basis number are square.
+-/
+
+
+variable {n m : Type _} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m]
+
+variable {R : Type _} [Semiring R] [InvariantBasisNumber R]
+
+open Matrix
+
+theorem Matrix.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)
+#align matrix.square_of_invertible Matrix.square_of_invertible
+