no goals
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : StrongRankCondition K
⊢ Module.rank K K = ↑1
simp