K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
v : V
n : v ≠ 0
h : ∀ (w : V), ∃ c, c • v = w
this : Nontrivial K
⊢ finrank K V = 1
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
v : V
n : v ≠ 0
h : ∀ (w : V), ∃ c, c • v = w
⊢ finrank K V = 1
haveI := nontrivial_of_invariantBasisNumber K
case intro
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
v : V
n : v ≠ 0
h : ∀ (w : V), ∃ c, c • v = w
this : Nontrivial K
b : Basis PUnit K V
⊢ finrank K V = 1
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
v : V
n : v ≠ 0
h : ∀ (w : V), ∃ c, c • v = w
this : Nontrivial K
⊢ finrank K V = 1
obtain ⟨b⟩ := (Basis.basis_singleton_iff.{u} PUnit).mpr ⟨v, n, h⟩
no goals
case intro
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
v : V
n : v ≠ 0
h : ∀ (w : V), ∃ c, c • v = w
this : Nontrivial K
b : Basis PUnit K V
⊢ finrank K V = 1
rw [finrank_eq_card_basis b, Fintype.card_punit]