## Stream: general

### Topic: zero vector space

#### Yury G. Kudryashov (Jan 03 2020 at 23:14):

Hi, is there any canonical way to say "a vector space is either {0}, or has a non-zero element"? I mean, are there any lemmas in linear_algebra that take some specific way of saying "E is not {0}" as an argument?

#### Alexander Bentkamp (Jan 05 2020 at 15:20):

I don't know what the canonical way to say it is, but maybe you could use these to lemmas that I proved recently, but haven't merged into mathlib yet:

lemma exists_mem_ne_zero_of_dim_pos' {α : Type v} {β : Type w}
[discrete_field α] [add_comm_group β] [vector_space α β]
(h_dim : 0 < dim α β) : ∃ x : β, x ≠ 0 :=
begin
obtain ⟨b, _, _⟩ : (∃ b : β, b ∈ (⊤ : submodule α β) ∧ b ≠ 0),
{ apply exists_mem_ne_zero_of_dim_pos,
rw dim_top,
apply h_dim },
use b
end

lemma dim_pos_of_mem_ne_zero {α : Type v} {β : Type w}
[discrete_field α] [add_comm_group β] [vector_space α β]
(x : β) (h : x ≠ 0) : 0 < dim α β :=
begin
classical,
by_contra hc,
rw [not_lt, cardinal.le_zero, ←dim_top] at hc,
have x_mem_bot : x ∈ ⊥,
{ rw ← submodule.bot_of_dim_zero ⊤ hc,
apply mem_top },
exact h ((mem_bot α).1 x_mem_bot)
end


Last updated: May 11 2021 at 00:31 UTC