case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ finrank K { x // x ∈ span K {v} } ≤ 1

case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ 1 ≤ finrank K { x // x ∈ span K {v} }
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ finrank K { x // x ∈ span K {v} } = 1
apply le_antisymm
no goals
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ finrank K { x // x ∈ span K {v} } ≤ 1
exact finrank_span_le_card ({v} : Set V)
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ Nontrivial { x // x ∈ span K {v} }
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ 1 ≤ finrank K { x // x ∈ span K {v} }
rw [Nat.succ_le_iff, finrank_pos_iff]
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ { val := v, property := (_ : v ∈ span K {v}) } ≠ 0
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ Nontrivial { x // x ∈ span K {v} }
use ⟨v, mem_span_singleton_self v⟩, 0
no goals
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ { val := v, property := (_ : v ∈ span K {v}) } ≠ 0
simp [hv]