findim_eq_one_iff

Stream: Is there code for X?

[Scott Morrison]

Do we have

lemma findim_eq_one_iff (v : V) (n : v ≠ 0) (h : ∀ w : V, ∃ c : K, w = c • v) :
  findim K V = 1 :=
sorry

and/or an easy path to it?

[Scott Morrison]

Perhaps best to have

lemma findim_le_one_iff (v : V) (h : ∀ w : V, ∃ c : K, w = c • v) :
  findim K V <= 1 :=
sorry

first?

[Scott Morrison]

#7354

[Eric Wieser]

Should we have these for dim too?

[Sebastien Gouezel]

By the way, #7322 renames dim and findim to rank and finrank. If you don't like it, it is still time to voice your concerns on the PR page :-)