Structures · Algebra

IsCyclotomicExtension

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

Shape

3 explicit arguments · adds exists_isPrimitiveRoot, adjoin_roots