Theorems · Theorem · commutative algebra

linearIndependent_pow

∀ {S : Type u_2} [inst : Ring S] {K : Type u_6} [inst_1 : Field K] [inst_2 : Algebra K S] (x : S),
  LinearIndependent K fun i => x ^ ↑i

Useful lemma to show x generates a power basis: the powers of x less than the degree of x's minimal polynomial are linearly independent.

Defined in

Mathlib.RingTheory.PowerBasis

Cited by

0 results in Mathlib

Foundations

Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingFieldAlgebra