Theorems · Theorem · field theory

Polynomial.aevalAevalEquiv_apply_apply

∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (xy : A × A)
  (x : Polynomial (Polynomial R)),
  ((Polynomial.aevalAevalEquiv R A) xy) x = Polynomial.eval xy.1 ((Polynomial.aeval (Polynomial.C xy.2)) x)

Defined in

Mathlib.Algebra.Polynomial.Bivariate

Cited by

16 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebra