zero vector space

Stream: general

[Yury G. Kudryashov]

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]

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