Invertible matrices over a ring with invariant basis number are square.

@[instance 100]

instance instIsStablyFiniteRingOfOrzechProperty {R : Type u_1} [Semiring R] [OrzechProperty R] : IsStablyFiniteRing R

@[instance 100]

instance instRankConditionOfIsStablyFiniteRingOfNontrivial {R : Type u_1} [Semiring R] [IsStablyFiniteRing R] [Nontrivial R] : RankCondition R

theorem rankCondition_iff_le_of_comp_eq_one {R : Type u_1} [Semiring R] : RankCondition R ↔ ∀ (n m : ℕ) (f : (Fin n → R) →ₗ[R] Fin m → R) (g : (Fin m → R) →ₗ[R] Fin n → R), f ∘ₗ g = 1 → m ≤ n

theorem rankCondition_iff_matrix {R : Type u_1} [Semiring R] : RankCondition R ↔ ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), g * f = 1 → m ≤ n

theorem invariantBasisNumber_iff_matrix {R : Type u_1} [Semiring R] : InvariantBasisNumber R ↔ ∀ (n m : ℕ) (f : Matrix (Fin n) (Fin m) R) (g : Matrix (Fin m) (Fin n) R), f * g = 1 → g * f = 1 → n = m

theorem MulOpposite.rankCondition_iff {R : Type u_1} [Semiring R] : RankCondition Rᵐᵒᵖ ↔ RankCondition R

The rank condition is left-right symmetric. Note that the strong rank condition is not left-right symmetric, see Remark (1.32) in §1.1D of [lam_1999].

theorem MulOpposite.invariantBasisNumber_iff {R : Type u_1} [Semiring R] : InvariantBasisNumber Rᵐᵒᵖ ↔ InvariantBasisNumber R

Invariant basis number is left-right symmetric.

instance instRankConditionMulOpposite {R : Type u_1} [Semiring R] [RankCondition R] : RankCondition Rᵐᵒᵖ

instance instInvariantBasisNumberMulOpposite {R : Type u_1} [Semiring R] [InvariantBasisNumber R] : InvariantBasisNumber Rᵐᵒᵖ

theorem Matrix.square_of_invertible {n : Type u_1} {m : Type u_2} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] {R : Type u_3} [Semiring R] [InvariantBasisNumber R] (M : Matrix n m R) (N : Matrix m n R) (h : M * N = 1) (h' : N * M = 1) : Fintype.card n = Fintype.card m

@[instance 100]

instance rankCondition_of_nontrivial_of_commSemiring {R : Type u_4} [CommSemiring R] [Nontrivial R] : RankCondition R

Nontrivial commutative semirings R satisfy the rank condition.

If R is moreover a ring, then it satisfies the strong rank condition, see commRing_strongRankCondition. It is unclear whether this generalizes to semirings.