Finite fields of definition for tensors

A finite collection of vectors after an algebraic extension of scalars is already defined over one finite intermediate field. No finite-dimensionality assumption on the vector space is needed.

theorem Set.exists_finiteDimensional_intermediateField_tensor_range {k : Type u_1} {K : Type u_2} {V : Type u_3} [Field k] [Field K] [Algebra k K] [Algebra.IsAlgebraic k K] [AddCommGroup V] [Module k V] (s : Set (TensorProduct k K V)) (hs : s.Finite) : ∃ (L : IntermediateField k K), FiniteDimensional k ↥L ∧ s ⊆ ↑(LinearMap.rTensor V L.val.toLinearMap).range

Finitely many tensors over an algebraic extension have a common finite field of definition.