Theorems · Theorem · number theory
Polynomial.map_cyclotomic
∀ (n : ℕ) {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S),
Polynomial.map f (Polynomial.cyclotomic n R) = Polynomial.cyclotomic n SThe definition of cyclotomic n R commutes with any ring homomorphism.
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 201 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semiringproof · cited by 13,802
- RingHomstatement and proof · cited by 10,189
- Ringstatement and proof · cited by 7,463
- Polynomialstatement and proof · cited by 5,681
- RingHom.compproof · cited by 899
- Polynomial.mapstatement and proof · cited by 806
- Int.castRingHomproof · cited by 254
- Polynomial.cyclotomicstatement and proof · cited by 130
- Polynomial.map_mapproof · cited by 75
- Polynomial.map_cyclotomic_intproof · cited by 21
Cited by15
Results whose statement or proof uses this declaration.
- Polynomial.isRoot_cyclotomic_iffproof · cited by 12
- IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducibleproof · cited by 4
- IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_rootsproof · cited by 3
- Polynomial.cyclotomic.eval_applyproof · cited by 2
- Polynomial.cyclotomic_expand_eq_cyclotomicproof · cited by 2
- Polynomial.cyclotomic_expand_eq_cyclotomic_mulproof · cited by 2
- IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomicproof · cited by 2
- IsPrimitiveRoot.minpoly_dvd_cyclotomicproof · cited by 1
- cyclotomic_prime_pow_comp_X_add_one_isEisensteinAtproof · cited by 1
- Polynomial.eval_one_cyclotomic_not_prime_powproof · cited by 1
- IsCyclotomicExtension.aeval_zetaproof · cited by 1
- Polynomial.cyclotomic_mul_prime_dvd_eq_powproof · cited by 1