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,

Mathlib/LinearAlgebra/Dimension/Finrank.lean

@@ -68,6 +68,9 @@ noncomputable def finrank (R M : Type*) [Semiring R] [AddCommMonoid M] [Module R
 theorem finrank_eq_of_rank_eq {n : ℕ} (h : Module.rank R M = ↑n) : finrank R M = n := by
   simp [finrank, h]
 
+theorem CommSemiring.finrank_self (R) [CommSemiring R] : Module.finrank R R = 1 :=
+  finrank_eq_of_rank_eq (rank_self R)
+
 lemma rank_eq_one_iff_finrank_eq_one : Module.rank R M = 1 ↔ finrank R M = 1 :=
   Cardinal.toNat_eq_one.symm