Theorems · Theorem · field theory

RatFunc.algEquivOfTranscendental_algebraMap

∀ {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) ((algebraMap (Polynomial K) (RatFunc K)) g) =
    (Polynomial.aeval (IntermediateField.AdjoinSimple.gen K f)) g

Defined in

Mathlib.FieldTheory.RatFunc.AsPolynomial

Cited by

3 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra