Theorems · Theorem · field theory

Polynomial.mapAlg_comp

∀ {A : Type u_3} (B : Type u_4) (C : Type u_5) [inst : CommSemiring A] [inst_1 : CommSemiring B] [inst_2 : Semiring C]
  [inst_3 : Algebra A B] [inst_4 : Algebra A C] [inst_5 : Algebra B C] [IsScalarTower A B C] (p : Polynomial A),
  (Polynomial.mapAlg A C) p = (Polynomial.mapAlg B C) ((Polynomial.mapAlg A B) p)

Defined in

Mathlib.Algebra.Polynomial.AlgebraMap

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringSemiringAlgebraAlgebraAlgebraIsScalarTower