Theorems · Theorem · field theory
Polynomial.pow_comp
∀ {R : Type u_1} [inst : CommSemiring R] (p q : Polynomial R) (n : ℕ), (p ^ n).comp q = p.comp q ^ n- Defined in
- Mathlib.Algebra.Polynomial.Eval.Defs
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommSemiringstatement and proof · cited by 10,911
- Polynomialstatement and proof · cited by 5,681
- Polynomial.compstatement and proof · cited by 193
- MonoidHom.map_powproof · cited by 30
- Polynomial.mul_compproof · cited by 24
- Polynomial.one_compproof · cited by 18
Cited by7
Results whose statement or proof uses this declaration.
- Polynomial.bernoulli_comp_one_sub_Xproof · cited by 2
- X_pow_mul_sub_C_irreducibleproof · cited by 1
- Polynomial.eval_divByMonic_eq_trailingCoeff_compproof · cited by 1
- Polynomial.neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eqproof · cited by 1
- bernsteinPolynomial.flipproof · cited by 1
- splits_X_pow_sub_one_of_X_pow_sub_Cproof · cited by 1
- cyclotomic_prime_pow_comp_X_add_one_isEisensteinAtproof · cited by 1