Theorems · Theorem · number theory

IsCyclotomicExtension.iff_adjoin_eq_top

∀ (S : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
  IsCyclotomicExtension S A B ↔
    (∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n) ∧ Algebra.adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} = ⊤

A reformulation of IsCyclotomicExtension that uses ⊤.

Defined in

Mathlib.NumberTheory.Cyclotomic.Basic

Cited by

13 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebra