Theorems · Theorem · number theory

IsCyclotomicExtension.of_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) → ∀ [H : 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 implies IsCyclotomicExtension (S ∪ {n}) A B.

Defined in

Mathlib.NumberTheory.Cyclotomic.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

NeZeroCommRingCommRingAlgebraIsCyclotomicExtension