Theorems · Theorem · field theory

RatFunc.algEquivOfTranscendental_apply

∀ {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) (u : RatFunc K),
  ↑((RatFunc.algEquivOfTranscendental f h) u) = (Polynomial.aeval f) u.num / (Polynomial.aeval f) u.denom

Defined in

Mathlib.FieldTheory.RatFunc.AsPolynomial

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra