Theorems · Theorem · number theory

IsCyclotomicExtension.iff_union_singleton_one

∀ (S : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
  IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {1}) A B

IsCyclotomicExtension S A B is equivalent to IsCyclotomicExtension (S ∪ {1}) A B.

Defined in

Mathlib.NumberTheory.Cyclotomic.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra