Theorems · Theorem · field theory

RatFunc.eval_algebraMap

∀ {K : Type u} [inst : Field K] {L : Type u} [inst_1 : Field L] (f : K →+* L) (a : L) {S : Type u_1}
  [inst_2 : CommSemiring S] [inst_3 : Algebra S (Polynomial K)] (p : S),
  RatFunc.eval f a ((algebraMap S (RatFunc K)) p) = Polynomial.eval₂ f a ((algebraMap S (Polynomial K)) p)

Defined in

Mathlib.FieldTheory.RatFunc.AsPolynomial

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldCommSemiringAlgebra