Theorems · Theorem · number theory
IsPrimitiveRoot.isRoot_cyclotomic
∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} [IsDomain R],
0 < n → ∀ {μ : R}, IsPrimitiveRoot μ n → (Polynomial.cyclotomic n R).IsRoot μAny n-th primitive root of unity is a root of cyclotomic n R.
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 206 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Polynomialproof · cited by 5,681
- Multisetproof · cited by 2,627
- IsDomainstatement and proof · cited by 2,196
- IsPrimitiveRootstatement and proof · cited by 356
- Polynomial.rootsproof · cited by 264
- Polynomial.IsRootstatement · cited by 152
- Polynomial.cyclotomicstatement · cited by 130
- primitiveRootsproof · cited by 57
- Polynomial.mem_rootsproof · cited by 30
- mem_primitiveRootsproof · cited by 18
- Finset.mem_defproof · cited by 15
Cited by4
Results whose statement or proof uses this declaration.
- IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_rootsproof · cited by 3
- IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomicproof · cited by 2
- IsCyclotomicExtension.Rat.Three.eta_sqproof · cited by 1
- IsPrimitiveRoot.minpoly_dvd_cyclotomicproof · cited by 1