Theorems · Theorem · number theory

IsCyclotomicExtension.mem_of_pow_eq_one

∀ (S : Set ℕ) {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [IsDomain B]
  (C : Subalgebra A B) [h : IsCyclotomicExtension S A ↥C] {m : ℕ} {ζ : B}, m ∈ S → m ≠ 0 → ζ ^ m = 1 → ζ ∈ C

Defined in

Mathlib.NumberTheory.Cyclotomic.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraIsDomainIsCyclotomicExtension