span of linear forms

Stream: maths

[Etienne Marion]

Hi! I want to prove the following. I have a finite dimensional vector space E and a family of linear forms indexed by f : I \to E*. I assume that for any z != 0, there exists i : I such that f(i)(z) != 0. I want to prove that I can find a basis of E* of the form (f(i_1), ..., f(i_n)).

The idea I had in mind was to prove that the family f spans E*, and then extract a basis from it. To do so, I wanted to use the following result: a linear form is in the span of a certain family of linear forms if and only if its kernel contains the intersection of the kernels of this family. Is this result in Mathlib? (or something alike?) I also wanted to ask if you had a better idea on how to prove this result (irl and in Lean). Thanks!

[Patrick Massot]

Maybe play with docs#Subspace.orderIsoFiniteDimensional or neighboring declarations?

[Etienne Marion]

Thanks, I'll have a look.

[Etienne Marion]

In the end I used docs#Submodule.exists_dual_map_eq_bot_of_lt_top, which got me a contradiction.