Theorems · Theorem · number theory

IsCyclotomicExtension.iff_union_of_dvd

∀ {n : ℕ} [NeZero n] {S : Set ℕ} (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Algebra A B], (∃ s ∈ S, s ≠ 0 ∧ n ∣ s) → (IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {n}) A B)

If there exists a nonzero s ∈ S such that n ∣ s, then IsCyclotomicExtension S A B if and only if IsCyclotomicExtension (S ∪ {n}) A B.

Defined in

Mathlib.NumberTheory.Cyclotomic.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

NeZeroCommRingCommRingAlgebra