Theorems · Definition · field theory

AlgebraicIndependent

{ι : Type u_1} →
  (R : Type u_3) → {A : Type u_5} → (ι → A) → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → Prop

AlgebraicIndependent R x states the family of elements x is algebraically independent over R, meaning that the canonical map out of the multivariable polynomial ring is injective.

Defined in

Mathlib.RingTheory.AlgebraicIndependent.Defs

Cited by

120 results in Mathlib

Foundations

Depth 95 from the axioms, rests on 1,888 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebra