comment + finrank version

Author: alreadydone

Mathlib/LinearAlgebra/Dimension/Basic.lean

@@ -229,6 +229,11 @@ theorem rank_eq_of_equiv_equiv (i : R → R') (j : M ≃+ M₁)
 end
 end Semiring
 
+/-- TODO: prove that nontrivial commutative semirings satisfy the strong rank condition,
+following *Free sets and free subsemimodules in a semimodule* by Yi-Jia Tan, Theorem 3.2.
+
+Rings `R` that fail the strong rank condition but satisfy `rank R R = 1` are expected to exist, see
+https://mathoverflow.net/questions/317422/rings-that-fail-to-satisfy-the-strong-rank-condition. -/
 theorem CommSemiring.rank_self (R) [CommSemiring R] : Module.rank R R = 1 := by
   nontriviality R
   rw [le_antisymm_iff, ← not_lt, ← Order.succ_le_iff, ← Nat.cast_one, ← nat_succ,
@@ -240,6 +245,9 @@ theorem CommSemiring.rank_self (R) [CommSemiring R] : Module.rank R R = 1 := by
   have h₂ : 0 = f ![1, 0] := by simpa using congr($this 1)
   exact zero_ne_one (α := R) (by simpa using congr($(inj (h₁.trans h₂)) 1))
 
+theorem CommSemiring.finrank_self (R) [CommSemiring R] : Module.finrank R R = 1 :=
+  Module.finrank_eq_of_rank_eq (rank_self R)
+
 section Ring
 variable [Ring R] [AddCommGroup M] [Module R M] [Ring R']