Theorems · Theorem · field theory

Polynomial.Bivariate.aveal_eq_map_swap

∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (x : A)
  (p : Polynomial (Polynomial R)),
  (Polynomial.aeval (Polynomial.C x)) p = (Polynomial.mapAlgHom (Polynomial.aeval x)) (Polynomial.Bivariate.swap p)

Defined in: Mathlib.Algebra.Polynomial.Bivariate
Cited by: 1 results in Mathlib
Foundations: Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring CommSemiring Algebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites36

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Algebrastatement and proof · cited by 11,388
CommSemiringstatement and proof · cited by 10,911
RingHomstatement · cited by 10,189
Polynomialstatement and proof · cited by 5,681
Algebra.algebraMapproof · cited by 4,706
AlgHomstatement · cited by 3,236
AlgEquivstatement · cited by 1,681
Polynomial.Xproof · cited by 1,639
Polynomial.Cstatement and proof · cited by 1,598
map_addproof · cited by 964
Polynomial.mapproof · cited by 806

Cited by1

Results whose statement or proof uses this declaration.

Polynomial.Bivariate.Transcendental.algEquivAdjoin_swap_eq_aevalproof · cited by 1