Linear independence from transcendence

The powers of a transcendental element of an algebra are linearly independent over the base ring.

Main results

• Transcendental.linearIndependent_pow: the powers of a transcendental element are linearly independent over the base ring.
• Transcendental.finrank_span_range_pow: over a field, the span of the first n powers of a transcendental element has dimension n.

theorem Transcendental.linearIndependent_pow {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] {x : A} (hx : Transcendental R x) : LinearIndependent R fun (n : ℕ) => x ^ n

The powers of a transcendental element are linearly independent over the base ring: they are the images of the monomial basis of R[X] under the injective evaluation map at x.

theorem Transcendental.finrank_span_range_pow {K : Type u_3} {B : Type u_4} [Field K] [Ring B] [Algebra K B] {x : B} (hx : Transcendental K x) (n : ℕ) : Module.finrank K ↥(Submodule.span K (Set.range fun (i : Fin n) => x ^ ↑i)) = n

The span of 1, x, …, x^{n-1} has dimension n for a transcendental element x of an algebra over a field.