Theorems · Definition · number theory
CyclotomicRing
ℕ → (A : Type u) → (K : Type w) → [inst : CommRing A] → [inst_1 : Field K] → [Algebra A K] → Type w
If A is a domain with fraction field K and n : ℕ, we define CyclotomicRing n A K as
the A-subalgebra of CyclotomicField n K generated by the roots of X ^ n - 1. If n
is nonzero in A, it has the instance IsCyclotomicExtension {n} A (CyclotomicRing n A K).
- Defined in
- Mathlib.NumberTheory.Cyclotomic.Basic
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 213 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- Fieldstatement and proof · cited by 7,404
- Set.ofPredproof · cited by 6,101
- Algebra.adjoinproof · cited by 535
- CyclotomicFieldproof · cited by 14
Cited by6
Results whose statement or proof uses this declaration.
- IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_powstatement and proof · cited by 1
- IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosurestatement and proof · cited by 0
- IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_primestatement and proof · cited by 0
- CyclotomicRing.adjoin_algebra_injectivestatement · cited by 0
- CyclotomicRing.algebraBase_injectivestatement and proof · cited by 0
- CyclotomicRing.eq_adjoin_primitive_rootstatement and proof · cited by 0