Theorems · Inductive type · number theory

IsCyclotomicExtension

Set ℕ → (A : Type u) → (B : Type v) → [inst : CommRing A] → [inst_1 : CommRing B] → [Algebra A B] → Prop

Given an A-algebra B and S : Set ℕ, we define IsCyclotomicExtension S A B requiring that there is an n-th primitive root of unity in B for all nonzero n ∈ S and that B is generated over A by the roots of X ^ n - 1.

Defined in

Mathlib.NumberTheory.Cyclotomic.Basic

Cited by

220 results in Mathlib

Foundations

Depth 6 from the axioms, rests on 24 definitions · uses no axioms

Assumes

CommRingCommRingAlgebra