Theorems · Definition · field theory

AlgebraicIndependent.reprField

{ι : Type u_1} →
  {F : Type u_2} →
    {E : Type u_3} →
      {x : ι → E} →
        [inst : Field F] →
          [inst_1 : Field E] →
            [inst_2 : Algebra F E] →
              AlgebraicIndependent F x →
                ↥(IntermediateField.adjoin F (Set.range x)) →ₐ[F] FractionRing (MvPolynomial ι F)

The canonical map from the intermediate field generated by an algebraic independent family into the rational function field.

Defined in

Mathlib.RingTheory.AlgebraicIndependent.Adjoin

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra