From 1cf0e90adea02b722edb0c54120c02304ad35a0d Mon Sep 17 00:00:00 2001
From: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>
Date: Fri, 19 Jun 2026 22:18:35 +0800
Subject: [PATCH] add lemma for span rank one

---
 Mathlib/Algebra/Module/SpanRank.lean | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/Mathlib/Algebra/Module/SpanRank.lean b/Mathlib/Algebra/Module/SpanRank.lean
index b987823c938eba..f0e93a10efe62b 100644
--- a/Mathlib/Algebra/Module/SpanRank.lean
+++ b/Mathlib/Algebra/Module/SpanRank.lean
@@ -284,6 +284,20 @@ lemma spanFinrank_singleton {m : M} (hm : m ≠ 0) : (span R {m}).spanFinrank =
   · by_contra!
     simp [Submodule.spanFinrank_eq_zero_iff_eq_bot (fg_span_singleton m), hm] at this
 
+lemma spanFinrank_eq_one_iff (p : Submodule R M) : p.spanFinrank = 1 ↔ p.IsPrincipal ∧ p ≠ ⊥ := by
+  refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨prin, ne⟩ ↦ ?_⟩
+  · have fg : p.FG := by
+      contrapose h
+      simp [Submodule.spanFinrank_of_not_fg h]
+    obtain ⟨a, ha⟩ : ∃ a, p.generators = {a} := by simpa [← fg.generators_ncard] using h
+    exact ⟨a, ha ▸ (p.span_generators).symm⟩
+  · contrapose h
+    simp [h]
+  · rcases prin with ⟨a, rfl⟩
+    apply Submodule.spanFinrank_singleton
+    contrapose ne
+    simp [ne]
+
 end Defs
 
 end Submodule