Theorems · Theorem · field theory

RatFunc.algEquivOfTranscendental_symm_aeval

∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (f : L)
  (h : Transcendental K f) (g : Polynomial K),
  (RatFunc.algEquivOfTranscendental f h).symm ((Polynomial.aeval (IntermediateField.AdjoinSimple.gen K f)) g) =
    (algebraMap (Polynomial K) (RatFunc K)) g

Defined in

Mathlib.FieldTheory.RatFunc.AsPolynomial

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra