Theorems · Theorem · field theory
Polynomial.aeval_X_pow
∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A) {n : ℕ},
(Polynomial.aeval x) (Polynomial.X ^ n) = x ^ n- Defined in
- Mathlib.Algebra.Polynomial.AlgebraMap
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 110 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiringSemiringAlgebra
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Semiringstatement and proof · cited by 13,802
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- Polynomialstatement · cited by 5,681
- AlgHomstatement · cited by 3,236
- Polynomial.Xstatement · cited by 1,639
- RingHomClass.toRingHomproof · cited by 746
- Polynomial.aevalstatement · cited by 615
- Algebra.ofIdproof · cited by 166
- Polynomial.eval₂_X_powproof · cited by 16
Cited by17
Results whose statement or proof uses this declaration.
- IsCyclotomicExtension.discr_prime_pow_ne_twoproof · cited by 4
- IsPurelyInseparable.elemExponent_le_of_pow_memproof · cited by 3
- PowerBasis.repr_gen_pow_isIntegralproof · cited by 2
- GaloisField.finrankproof · cited by 2
- IsAlgebraic.exists_nonzero_coeff_and_aeval_eq_zeroproof · cited by 2
- IsPrimitiveRoot.minpoly_dvd_x_pow_sub_oneproof · cited by 2
- gal_X_pow_sub_C_isSolvable_auxproof · cited by 1
- gal_X_pow_sub_one_isSolvableproof · cited by 1
- Module.AEval.X_pow_smul_ofproof · cited by 1
- LinearMap.isNilpotent_iff_charpolyproof · cited by 1
- spectrum.pow_image_subsetproof · cited by 1
- Module.End.eq_zero_of_isNilpotent_isSemisimpleproof · cited by 1