Loogle!

Result

Found 236 declarations mentioning IsCyclotomicExtension. Of these, only the first 200 are shown.

• IsCyclotomicExtension 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] : Prop
• IsCyclotomicExtension.integral 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension S A B] : Algebra.IsIntegral A B
• IsSepClosedOfCharZero.isCyclotomicExtension 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (K : Type w) [Field K] [IsSepClosed K] [CharZero K] (S : Set ℕ) : IsCyclotomicExtension S K K
• IsCyclotomicExtension.isAbelianGalois 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension S K L] : IsAbelianGalois K L
• IsCyclotomicExtension.isGalois 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension S K L] : IsGalois K L
• IsCyclotomicExtension.instSubsingleton 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [h : IsCyclotomicExtension ∅ A B] : Subsingleton (Subalgebra A B)
• CyclotomicField.instIsCyclotomicExtensionSingletonNatSetOfCharZero 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (n : ℕ) (K : Type w) [Field K] [CharZero K] : IsCyclotomicExtension {n} K (CyclotomicField n K)
• IsCyclotomicExtension.numberField 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [h : NumberField K] [Finite ↑S] [IsCyclotomicExtension S K L] : NumberField L
• IsCyclotomicExtension.isSeparable 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension S K L] : Algebra.IsSeparable K L
• IsCyclotomicExtension.iff_union_singleton_one 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] : IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {1}) A B
• IsCyclotomicExtension.eq_self_sdiff_zero 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] : IsCyclotomicExtension S A B = IsCyclotomicExtension (S \ {0}) A B
• CyclotomicField.instIsCyclotomicExtensionSingletonNatSetOfNat 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (K : Type w) [Field K] : IsCyclotomicExtension {0} K (CyclotomicField 0 K)
• IsCyclotomicExtension.exists_isPrimitiveRoot 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  {S : Set ℕ} (A : Type u) (B : Type v) {inst✝ : CommRing A} {inst✝¹ : CommRing B} {inst✝² : Algebra A B} [self : IsCyclotomicExtension S A B] {n : ℕ} (ha : n ∈ S) (ha' : n ≠ 0) : ∃ r, IsPrimitiveRoot r n
• IsCyclotomicExtension.subsingleton_iff 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [Subsingleton B] : IsCyclotomicExtension S A B ↔ S ⊆ {0, 1}
• IsCyclotomicExtension.splitting_field_cyclotomic 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (n : ℕ) [NeZero n] (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension {n} K L] : Polynomial.IsSplittingField K L (Polynomial.cyclotomic n K)
• IsCyclotomicExtension.union_of_isPrimitiveRoot 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  {n : ℕ} [NeZero n] (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [hB : IsCyclotomicExtension S A B] {r : B} (hr : IsPrimitiveRoot r n) : IsCyclotomicExtension (S ∪ {n}) A B
• IsCyclotomicExtension.finite 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [IsDomain B] [h₁ : Finite ↑S] [h₂ : IsCyclotomicExtension S A B] : Module.Finite A B
• CyclotomicField.isCyclotomicExtension 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (n : ℕ) [NeZero n] (K : Type w) [Field K] [NeZero ↑n] : IsCyclotomicExtension {n} K (CyclotomicField n K)
• IsCyclotomicExtension.equiv 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] {C : Type u_1} [CommRing C] [Algebra A C] [h : IsCyclotomicExtension S A B] (f : B ≃ₐ[A] C) : IsCyclotomicExtension S A C
• IsCyclotomicExtension.finiteDimensional 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) (K : Type w) [Field K] (C : Type z) [Finite ↑S] [CommRing C] [Algebra K C] [IsDomain C] [IsCyclotomicExtension S K C] : FiniteDimensional K C
• IsCyclotomicExtension.neZero 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (n : ℕ) [NeZero n] (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} A B] [IsDomain B] : NeZero ↑n
• IsCyclotomicExtension.neZero' 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (n : ℕ) [NeZero n] (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} A B] [IsDomain B] : NeZero ↑n
• IsSepClosed.isCyclotomicExtension 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) (K : Type w) [Field K] [IsSepClosed K] (h : ∀ a ∈ S, a ≠ 0 → NeZero ↑a) : IsCyclotomicExtension S K K
• IsCyclotomicExtension.finite_of_singleton 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (n : ℕ) [NeZero n] (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [IsDomain B] [h : IsCyclotomicExtension {n} A B] : Module.Finite A B
• IsCyclotomicExtension.neZero_of_mem 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (n : ℕ) [NeZero n] (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension S A B] [IsDomain B] (hn : n ∈ S) : NeZero ↑n
• IsCyclotomicExtension.neZero_of_mem' 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (n : ℕ) [NeZero n] (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension S A B] [IsDomain B] (hn : n ∈ S) : NeZero ↑n
• IsCyclotomicExtension.of_union_of_dvd 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  {n : ℕ} [NeZero n] {S : Set ℕ} (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] (h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s) [H : IsCyclotomicExtension S A B] : IsCyclotomicExtension (S ∪ {n}) A B
• IsCyclotomicExtension.iff_union_of_dvd 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  {n : ℕ} [NeZero n] {S : Set ℕ} (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] (h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s) : IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {n}) A B
• IsCyclotomicExtension.singleton_one_of_algebraMap_bijective 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] (h : Function.Surjective ⇑(algebraMap A B)) : IsCyclotomicExtension {1} A B
• IsCyclotomicExtension.algEquiv 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension S K L] (L' : Type u_1) [Field L'] [Algebra K L'] [IsCyclotomicExtension S K L'] : L ≃ₐ[K] L'
• IsCyclotomicExtension.isCyclotomicExtension_zero_iff 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] : IsCyclotomicExtension {0} A B ↔ Function.Surjective ⇑(algebraMap A B)
• CyclotomicRing.isCyclotomicExtension 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (n : ℕ) [NeZero n] (A : Type u) (K : Type w) [CommRing A] [Field K] [Algebra A K] [IsDomain A] [IsFractionRing A K] [NeZero ↑n] : IsCyclotomicExtension {n} A (CyclotomicRing n A K)
• IsCyclotomicExtension.splits_cyclotomic 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  {n : ℕ} [NeZero n] {S : Set ℕ} (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension S K L] (hS : n ∈ S) : (Polynomial.map (algebraMap K L) (Polynomial.cyclotomic n K)).Splits
• IsCyclotomicExtension.adjoin_roots 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  {S : Set ℕ} {A : Type u} {B : Type v} {inst✝ : CommRing A} {inst✝¹ : CommRing B} {inst✝² : Algebra A B} [self : IsCyclotomicExtension S A B] (x : B) : x ∈ Algebra.adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}
• IsCyclotomicExtension.iff_singleton 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (n : ℕ) [NeZero n] (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] : IsCyclotomicExtension {n} A B ↔ (∃ r, IsPrimitiveRoot r n) ∧ ∀ (x : B), x ∈ Algebra.adjoin A {b | b ^ n = 1}
• IsPrimitiveRoot.adjoin_isCyclotomicExtension 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (A : Type u) {B : Type v} [CommRing A] [CommRing B] [Algebra A B] {ζ : B} {n : ℕ} [NeZero n] (h : IsPrimitiveRoot ζ n) : IsCyclotomicExtension {n} A ↥A[ζ]
• isCyclotomicExtension_singleton_iff_eq_adjoin 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (n : ℕ) [NeZero n] {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [IsDomain B] (C : Subalgebra A B) {ζ : B} (hζ : IsPrimitiveRoot ζ n) : IsCyclotomicExtension {n} A ↥C ↔ C = A[ζ]
• IsCyclotomicExtension.isMulCommutative 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension S A B] [IsDomain B] : IsMulCommutative (B ≃ₐ[A] B)
• IsCyclotomicExtension.trans 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S T : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] (C : Type w) [CommRing C] [Algebra A C] [Algebra B C] [IsScalarTower A B C] [hS : IsCyclotomicExtension S A B] [hT : IsCyclotomicExtension T B C] (h : Function.Injective ⇑(algebraMap B C)) : IsCyclotomicExtension (S ∪ T) A C
• IsCyclotomicExtension.mk 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  {S : Set ℕ} {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] (exists_isPrimitiveRoot : ∀ {n : ℕ}, n ∈ S → n ≠ 0 → ∃ r, IsPrimitiveRoot r n) (adjoin_roots : ∀ (x : B), x ∈ Algebra.adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) : IsCyclotomicExtension S A B
• isCyclotomicExtension_iff 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] : IsCyclotomicExtension S A B ↔ (∀ {n : ℕ}, n ∈ S → n ≠ 0 → ∃ r, IsPrimitiveRoot r n) ∧ ∀ (x : B), x ∈ Algebra.adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}
• IsCyclotomicExtension.eq 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [IsDomain B] (C₁ C₂ : Subalgebra A B) [h₁ : IsCyclotomicExtension S A ↥C₁] [h₂ : IsCyclotomicExtension S A ↥C₂] : C₁ = C₂
• IsCyclotomicExtension.mem_of_pow_eq_one 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [IsDomain B] (C : Subalgebra A B) [h : IsCyclotomicExtension S A ↥C] {m : ℕ} {ζ : B} (h₁ : m ∈ S) (h₂ : m ≠ 0) (hζ : ζ ^ m = 1) : ζ ∈ C
• IsCyclotomicExtension.isSplittingField_X_pow_sub_one 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (n : ℕ) [NeZero n] (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension {n} K L] : Polynomial.IsSplittingField K L (Polynomial.X ^ n - 1)
• IsCyclotomicExtension.algEquiv_eq_of_apply_eq 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension S A B] [IsDomain B] {f g : B ≃ₐ[A] B} (H : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n ∧ f r = g r) : f = g
• isCyclotomicExtension_iff_eq_adjoin 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [IsDomain B] (C : Subalgebra A B) (hS : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n) : IsCyclotomicExtension S A ↥C ↔ C = Algebra.adjoin A {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
• IntermediateField.isCyclotomicExtension_singleton_iff_eq_adjoin 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (n : ℕ) [NeZero n] (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] (F : IntermediateField K L) {ζ : L} (hζ : IsPrimitiveRoot ζ n) : IsCyclotomicExtension {n} K ↥F ↔ F = K⟮ζ⟯
• IsCyclotomicExtension.splits_X_pow_sub_one 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  {n : ℕ} [NeZero n] {S : Set ℕ} (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [H : IsCyclotomicExtension S K L] (hS : n ∈ S) : (Polynomial.map (algebraMap K L) (Polynomial.X ^ n - 1)).Splits
• IsCyclotomicExtension.le_of_dvd 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [IsDomain B] (n₁ n₂ : ℕ) (C₁ C₂ : Subalgebra A B) [h₁ : IsCyclotomicExtension {n₁} A ↥C₁] [h₂ : IsCyclotomicExtension {n₂} A ↥C₂] [NeZero n₂] (h : n₁ ∣ n₂) : C₁ ≤ C₂
• IsPrimitiveRoot.intermediateField_adjoin_isCyclotomicExtension 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (K : Type w) {L : Type z} [Field K] [Field L] [Algebra K L] [Algebra.IsIntegral K L] {n : ℕ} [NeZero n] {ζ : L} (hζ : IsPrimitiveRoot ζ n) : IsCyclotomicExtension {n} K ↥K⟮ζ⟯
• IsCyclotomicExtension.adjoin_primitive_root_eq_top 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] {n : ℕ} [NeZero n] [IsDomain B] [h : IsCyclotomicExtension {n} A B] {ζ : B} (hζ : IsPrimitiveRoot ζ n) : A[ζ] = ⊤
• IsCyclotomicExtension.union_left 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S T : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [h : IsCyclotomicExtension T A B] (hS : S ⊆ T) : IsCyclotomicExtension S A ↥(Algebra.adjoin A {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
• IsCyclotomicExtension.union_right 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S T : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [h : IsCyclotomicExtension (S ∪ T) A B] : IsCyclotomicExtension T (↥(Algebra.adjoin A {b | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B
• Algebra.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] (h : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n) : IsCyclotomicExtension S A ↥(Algebra.adjoin A {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
• IsCyclotomicExtension.iff_adjoin_eq_top 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) (A : Type u) (B : Type v) [CommRing A] [CommRing B] [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} = ⊤
• IntermediateField.isCyclotomicExtension_eq 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] (F₁ F₂ : IntermediateField K L) [h₁ : IsCyclotomicExtension S K ↥F₁] [h₂ : IsCyclotomicExtension S K ↥F₂] : F₁ = F₂
• IntermediateField.isCyclotomicExtension_le_of_dvd 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] (n₁ n₂ : ℕ) (F₁ F₂ : IntermediateField K L) [h₁ : IsCyclotomicExtension {n₁} K ↥F₁] [h₂ : IsCyclotomicExtension {n₂} K ↥F₂] [NeZero n₂] (h : n₁ ∣ n₂) : F₁ ≤ F₂
• IsCyclotomicExtension.singleton_one 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B] [h : IsCyclotomicExtension {1} A B] : ⊥ = ⊤
• IsCyclotomicExtension.singleton_one_of_bot_eq_top 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] (h : ⊥ = ⊤) : IsCyclotomicExtension {1} A B
• IsCyclotomicExtension.singleton_zero_of_bot_eq_top 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] (h : ⊥ = ⊤) : IsCyclotomicExtension {0} A B
• IntermediateField.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] (h : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n) : IsCyclotomicExtension S K ↥(IntermediateField.adjoin K {b | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
• IsCyclotomicExtension.lcm_sup 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [IsDomain B] (n₁ n₂ : ℕ) (C₁ C₂ : Subalgebra A B) [h₁ : IsCyclotomicExtension {n₁} A ↥C₁] [h₂ : IsCyclotomicExtension {n₂} A ↥C₂] [NeZero n₁] [NeZero n₂] : IsCyclotomicExtension {n₁.lcm n₂} A ↥(C₁ ⊔ C₂)
• IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_isSepClosed 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension S K L] (M : Type u_1) [Field M] [Algebra K M] [IsSepClosed M] : Nonempty (L ≃ₐ[K] ↥(IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))
• IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_exists_isPrimitiveRoot 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (S : Set ℕ) (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension S K L] (M : Type u_1) [Field M] [Algebra K M] (h : ∀ n ∈ S, n ≠ 0 → ∃ r, IsPrimitiveRoot r n) : Nonempty (L ≃ₐ[K] ↥(IntermediateField.adjoin K {x | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))
• IntermediateField.isCyclotomicExtension_lcm_sup 📋 Mathlib.NumberTheory.Cyclotomic.Basic
  (K : Type w) (L : Type z) [Field K] [Field L] [Algebra K L] (n₁ n₂ : ℕ) (F₁ F₂ : IntermediateField K L) [h₁ : IsCyclotomicExtension {n₁} K ↥F₁] [h₂ : IsCyclotomicExtension {n₂} K ↥F₂] [NeZero n₁] [NeZero n₂] : IsCyclotomicExtension {n₁.lcm n₂} K ↥(F₁ ⊔ F₂)
• IsCyclotomicExtension.zeta 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  (n : ℕ) [NeZero n] (A : Type w) (B : Type z) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} A B] : B
• IsCyclotomicExtension.zeta_spec 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  (n : ℕ) [NeZero n] (A : Type w) (B : Type z) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} A B] : IsPrimitiveRoot (IsCyclotomicExtension.zeta n A B) n
• IsPrimitiveRoot.powerBasis 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {n : ℕ} [NeZero n] (K : Type u) {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) : PowerBasis K L
• IsPrimitiveRoot.subOnePowerBasis 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {n : ℕ} [NeZero n] (K : Type u) {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) : PowerBasis K L
• IsPrimitiveRoot.dvd_of_isCyclotomicExtension 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  (n : ℕ) [NeZero n] {K : Type u} [Field K] [NumberField K] [IsCyclotomicExtension {n} ℚ K] {ζ : K} {l : ℕ} (hζ : IsPrimitiveRoot ζ l) (hl : l ≠ 0) : l ∣ 2 * n
• IsCyclotomicExtension.zeta_pow 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  (n : ℕ) [NeZero n] (A : Type w) (B : Type z) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} A B] : IsCyclotomicExtension.zeta n A B ^ n = 1
• IsPrimitiveRoot.powerBasis_gen 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {n : ℕ} [NeZero n] (K : Type u) {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) : (IsPrimitiveRoot.powerBasis K hζ).gen = ζ
• IsCyclotomicExtension.zeta_isRoot 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  (n : ℕ) [NeZero n] (A : Type w) (B : Type z) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} A B] [IsDomain B] [NeZero ↑n] : (Polynomial.cyclotomic n B).IsRoot (IsCyclotomicExtension.zeta n A B)
• IsPrimitiveRoot.powerBasis_dim 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {n : ℕ} [NeZero n] (K : Type u) {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) : (IsPrimitiveRoot.powerBasis K hζ).dim = (minpoly K ζ).natDegree
• IsPrimitiveRoot.exists_neg_pow_of_isOfFinOrder 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {n : ℕ} [NeZero n] {K : Type u} [Field K] [NumberField K] [IsCyclotomicExtension {n} ℚ K] (hno : Odd n) {ζ x : K} (hζ : IsPrimitiveRoot ζ n) (hx : IsOfFinOrder x) : ∃ r, x = (-ζ) ^ r
• IsPrimitiveRoot.subOnePowerBasis_gen 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {n : ℕ} [NeZero n] (K : Type u) {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) : (IsPrimitiveRoot.subOnePowerBasis K hζ).gen = ζ - 1
• IsCyclotomicExtension.finrank 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {n : ℕ} [NeZero n] {K : Type u} (L : Type v) [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] (hirr : Irreducible (Polynomial.cyclotomic n K)) : Module.finrank K L = n.totient
• IsPrimitiveRoot.subOnePowerBasis_dim 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {n : ℕ} [NeZero n] (K : Type u) {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) : (IsPrimitiveRoot.subOnePowerBasis K hζ).dim = (minpoly K (ζ - 1)).natDegree
• IsPrimitiveRoot.exists_pow_or_neg_mul_pow_of_isOfFinOrder 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {n : ℕ} [NeZero n] {K : Type u} [Field K] [NumberField K] [IsCyclotomicExtension {n} ℚ K] (hno : Odd n) {ζ x : K} (hζ : IsPrimitiveRoot ζ n) (hx : IsOfFinOrder x) : ∃ r < n, x = ζ ^ r ∨ x = -ζ ^ r
• IsPrimitiveRoot.embeddingsEquivPrimitiveRoots 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {n : ℕ} [NeZero n] {K : Type u} {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) (C : Type u_1) [CommRing C] [IsDomain C] [Algebra K C] (hirr : Irreducible (Polynomial.cyclotomic n K)) : (L →ₐ[K] C) ≃ ↥(primitiveRoots n C)
• IsPrimitiveRoot.powerBasis_gen_mem_adjoin_zeta_sub_one 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {n : ℕ} [NeZero n] (K : Type u) {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) : (IsPrimitiveRoot.powerBasis K hζ).gen ∈ K[ζ - 1]
• IsPrimitiveRoot.norm_eq_one 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {n : ℕ} [NeZero n] {K : Type u} {L : Type v} [CommRing L] {ζ : L} [Field K] [Algebra K L] (hζ : IsPrimitiveRoot ζ n) [IsDomain L] [IsCyclotomicExtension {n} K L] (hn : n ≠ 2) (hirr : Irreducible (Polynomial.cyclotomic n K)) : (Algebra.norm K) ζ = 1
• IsCyclotomicExtension.norm_zeta_eq_one 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {n : ℕ} [NeZero n] {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension {n} K L] (hn : n ≠ 2) (hirr : Irreducible (Polynomial.cyclotomic n K)) : (Algebra.norm K) (IsCyclotomicExtension.zeta n K L) = 1
• IsCyclotomicExtension.aeval_zeta 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  (n : ℕ) [NeZero n] (A : Type w) (B : Type z) [CommRing A] [CommRing B] [Algebra A B] [IsCyclotomicExtension {n} A B] [IsDomain B] [NeZero ↑n] : (Polynomial.aeval (IsCyclotomicExtension.zeta n A B)) (Polynomial.cyclotomic n A) = 0
• IsPrimitiveRoot.norm_sub_one_of_prime_ne_two' 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {p : ℕ} {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] [hpri : Fact (Nat.Prime p)] [hcyc : IsCyclotomicExtension {p} K L] (hζ : IsPrimitiveRoot ζ p) (hirr : Irreducible (Polynomial.cyclotomic p K)) (h : p ≠ 2) : (Algebra.norm K) (ζ - 1) = ↑p
• IsPrimitiveRoot.sub_one_norm_isPrimePow 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {n : ℕ} [NeZero n] {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] (hζ : IsPrimitiveRoot ζ n) (hn : IsPrimePow n) [IsCyclotomicExtension {n} K L] (hirr : Irreducible (Polynomial.cyclotomic n K)) (h : n ≠ 2) : (Algebra.norm K) (ζ - 1) = ↑n.minFac
• IsPrimitiveRoot.norm_of_cyclotomic_irreducible 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {n : ℕ} [NeZero n] {K : Type u} {L : Type v} [CommRing L] {ζ : L} [Field K] [Algebra K L] (hζ : IsPrimitiveRoot ζ n) [IsDomain L] [IsCyclotomicExtension {n} K L] (hirr : Irreducible (Polynomial.cyclotomic n K)) : (Algebra.norm K) ζ = if n = 2 then -1 else 1
• IsCyclotomicExtension.norm_zeta_sub_one_of_isPrimePow 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {n : ℕ} [NeZero n] {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] (hn : IsPrimePow n) [IsCyclotomicExtension {n} K L] (hirr : Irreducible (Polynomial.cyclotomic n K)) (h : n ≠ 2) : (Algebra.norm K) (IsCyclotomicExtension.zeta n K L - 1) = ↑n.minFac
• IsCyclotomicExtension.norm_zeta_sub_one_of_prime_ne_two 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {p : ℕ} {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] [Fact (Nat.Prime p)] [IsCyclotomicExtension {p} K L] (hirr : Irreducible (Polynomial.cyclotomic p K)) (h : p ≠ 2) : (Algebra.norm K) (IsCyclotomicExtension.zeta p K L - 1) = ↑p
• IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomic 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {n : ℕ} [NeZero n] {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] (hζ : IsPrimitiveRoot ζ n) [IsCyclotomicExtension {n} K L] (h : 2 < n) (hirr : Irreducible (Polynomial.cyclotomic n K)) : (Algebra.norm K) (ζ - 1) = ↑(Polynomial.eval 1 (Polynomial.cyclotomic n ℤ))
• IsPrimitiveRoot.minpoly_sub_one_eq_cyclotomic_comp 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {n : ℕ} [NeZero n] {A : Type w} {K : Type u} [CommRing A] [Field K] [Algebra K A] [IsDomain A] {ζ : A} [IsCyclotomicExtension {n} K A] (hζ : IsPrimitiveRoot ζ n) (h : Irreducible (Polynomial.cyclotomic n K)) : minpoly K (ζ - 1) = (Polynomial.cyclotomic n K).comp (Polynomial.X + 1)
• IsPrimitiveRoot.norm_sub_one_two 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] {k : ℕ} (hζ : IsPrimitiveRoot ζ (2 ^ k)) (hk : 2 ≤ k) [H : IsCyclotomicExtension {2 ^ k} K L] (hirr : Irreducible (Polynomial.cyclotomic (2 ^ k) K)) : (Algebra.norm K) (ζ - 1) = 2
• IsPrimitiveRoot.norm_sub_one_of_prime_ne_two 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {p : ℕ} {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] {k : ℕ} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) [hpri : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic (p ^ (k + 1)) K)) (h : p ≠ 2) : (Algebra.norm K) (ζ - 1) = ↑p
• IsCyclotomicExtension.norm_zeta_pow_sub_one_two 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] {k : ℕ} (hk : 2 ≤ k) [IsCyclotomicExtension {2 ^ k} K L] (hirr : Irreducible (Polynomial.cyclotomic (2 ^ k) K)) : (Algebra.norm K) (IsCyclotomicExtension.zeta (2 ^ k) K L - 1) = 2
• IsCyclotomicExtension.norm_zeta_pow_sub_one_of_prime_ne_two 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {p : ℕ} {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] {k : ℕ} [Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic (p ^ (k + 1)) K)) (h : p ≠ 2) : (Algebra.norm K) (IsCyclotomicExtension.zeta (p ^ (k + 1)) K L - 1) = ↑p
• IsPrimitiveRoot.norm_pow_sub_one_eq_prime_pow_of_ne_zero 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {p : ℕ} {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] {k s : ℕ} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) [hpri : Fact (Nat.Prime p)] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic (p ^ (k + 1)) K)) (hs : s ≤ k) (hk : k ≠ 0) : (Algebra.norm K) (ζ ^ p ^ s - 1) = ↑p ^ p ^ s
• IsPrimitiveRoot.norm_pow_sub_one_of_prime_ne_two 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {p : ℕ} {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] {k : ℕ} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) [hpri : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic (p ^ (k + 1)) K)) {s : ℕ} (hs : s ≤ k) (hodd : p ≠ 2) : (Algebra.norm K) (ζ ^ p ^ s - 1) = ↑p ^ p ^ s
• IsPrimitiveRoot.norm_pow_sub_one_of_prime_pow_ne_two 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {p : ℕ} {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] {k s : ℕ} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) [hpri : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic (p ^ (k + 1)) K)) (hs : s ≤ k) (htwo : p ^ (k - s + 1) ≠ 2) : (Algebra.norm K) (ζ ^ p ^ s - 1) = ↑p ^ p ^ s
• IsPrimitiveRoot.norm_pow_sub_one_two 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {K : Type u} {L : Type v} [Field L] {ζ : L} [Field K] [Algebra K L] {k : ℕ} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) [IsCyclotomicExtension {2 ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic (2 ^ (k + 1)) K)) : (Algebra.norm K) (ζ ^ 2 ^ k - 1) = (-2) ^ 2 ^ k
• IsCyclotomicExtension.norm_zeta_pow_sub_one_of_prime_pow_ne_two 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {p : ℕ} {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] {k : ℕ} [Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K L] (hirr : Irreducible (Polynomial.cyclotomic (p ^ (k + 1)) K)) {s : ℕ} (hs : s ≤ k) (htwo : p ^ (k - s + 1) ≠ 2) : (Algebra.norm K) (IsCyclotomicExtension.zeta (p ^ (k + 1)) K L ^ p ^ s - 1) = ↑p ^ p ^ s
• IsPrimitiveRoot.embeddingsEquivPrimitiveRoots_apply_coe 📋 Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
  {n : ℕ} [NeZero n] {K : Type u} {L : Type v} [Field K] [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n) (C : Type u_1) [CommRing C] [IsDomain C] [Algebra K C] (hirr : Irreducible (Polynomial.cyclotomic n K)) (φ' : L →ₐ[K] C) : ↑((hζ.embeddingsEquivPrimitiveRoots C hirr) φ') = φ' ζ
• IsCyclotomicExtension.discr_odd_prime 📋 Mathlib.NumberTheory.Cyclotomic.Discriminant
  {p : ℕ} {K : Type u} {L : Type v} {ζ : L} [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension {p} K L] [hp : Fact (Nat.Prime p)] (hζ : IsPrimitiveRoot ζ p) (hirr : Irreducible (Polynomial.cyclotomic p K)) (hodd : p ≠ 2) : Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ ((p - 1) / 2) * ↑p ^ (p - 2)
• IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow 📋 Mathlib.NumberTheory.Cyclotomic.Discriminant
  {p k : ℕ} {K : Type u} {L : Type v} {ζ : L} [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension {p ^ k} K L] [hp : Fact (Nat.Prime p)] (hζ : IsPrimitiveRoot ζ (p ^ k)) (hirr : Irreducible (Polynomial.cyclotomic (p ^ k) K)) : ∃ u n, Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = ↑↑u * ↑p ^ n
• IsPrimitiveRoot.discr_zeta_eq_discr_zeta_sub_one 📋 Mathlib.NumberTheory.Cyclotomic.Discriminant
  {n : ℕ} [NeZero n] {K : Type u} [Field K] [CharZero K] {ζ : K} [ce : IsCyclotomicExtension {n} ℚ K] (hζ : IsPrimitiveRoot ζ n) : Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis = Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis
• IsCyclotomicExtension.discr_prime_pow 📋 Mathlib.NumberTheory.Cyclotomic.Discriminant
  {p k : ℕ} {K : Type u} {L : Type v} {ζ : L} [Field K] [Field L] [Algebra K L] [hcycl : IsCyclotomicExtension {p ^ k} K L] [hp : Fact (Nat.Prime p)] (hζ : IsPrimitiveRoot ζ (p ^ k)) (hirr : Irreducible (Polynomial.cyclotomic (p ^ k) K)) : Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ ((p ^ k).totient / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
• IsCyclotomicExtension.discr_prime_pow_ne_two 📋 Mathlib.NumberTheory.Cyclotomic.Discriminant
  {p k : ℕ} {K : Type u} {L : Type v} {ζ : L} [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension {p ^ (k + 1)} K L] [hp : Fact (Nat.Prime p)] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hirr : Irreducible (Polynomial.cyclotomic (p ^ (k + 1)) K)) (hk : p ^ (k + 1) ≠ 2) : Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ ((p ^ (k + 1)).totient / 2) * ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
• IsCyclotomicExtension.discr_prime_pow_ne_two' 📋 Mathlib.NumberTheory.Cyclotomic.Discriminant
  {p k : ℕ} {K : Type u} {L : Type v} {ζ : L} [Field K] [Field L] [Algebra K L] [IsCyclotomicExtension {p ^ (k + 1)} K L] [hp : Fact (Nat.Prime p)] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hirr : Irreducible (Polynomial.cyclotomic (p ^ (k + 1)) K)) (hk : p ^ (k + 1) ≠ 2) : Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ (p ^ k * (p - 1) / 2) * ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
• IsCyclotomicExtension.fromZetaAut 📋 Mathlib.NumberTheory.Cyclotomic.Gal
  {n : ℕ} [NeZero n] {K : Type u_1} [Field K] {L : Type u_2} {μ : L} [CommRing L] [IsDomain L] (hμ : IsPrimitiveRoot μ n) [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic n K)) : L ≃ₐ[K] L
• IsCyclotomicExtension.fromZetaAut_spec 📋 Mathlib.NumberTheory.Cyclotomic.Gal
  {n : ℕ} [NeZero n] {K : Type u_1} [Field K] {L : Type u_2} {μ : L} [CommRing L] [IsDomain L] (hμ : IsPrimitiveRoot μ n) [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic n K)) : (IsCyclotomicExtension.fromZetaAut hμ h) (IsCyclotomicExtension.zeta n K L) = μ
• galCyclotomicEquivUnitsZMod 📋 Mathlib.NumberTheory.Cyclotomic.Gal
  {n : ℕ} [NeZero n] {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic n K)) : (Polynomial.cyclotomic n K).Gal ≃* (ZMod n)ˣ
• IsCyclotomicExtension.autEquivPow 📋 Mathlib.NumberTheory.Cyclotomic.Gal
  {n : ℕ} [NeZero n] {K : Type u_1} [Field K] (L : Type u_2) [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic n K)) : (L ≃ₐ[K] L) ≃* (ZMod n)ˣ
• IsPrimitiveRoot.autToPow_injective 📋 Mathlib.NumberTheory.Cyclotomic.Gal
  {n : ℕ} [NeZero n] (K : Type u_1) [Field K] {L : Type u_2} {μ : L} [CommRing L] [IsDomain L] (hμ : IsPrimitiveRoot μ n) [Algebra K L] [IsCyclotomicExtension {n} K L] : Function.Injective ⇑(IsPrimitiveRoot.autToPow K hμ)
• IsCyclotomicExtension.autEquivPow_symm_apply 📋 Mathlib.NumberTheory.Cyclotomic.Gal
  {n : ℕ} [NeZero n] {K : Type u_1} [Field K] (L : Type u_2) [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic n K)) (t : (ZMod n)ˣ) : (IsCyclotomicExtension.autEquivPow L h).symm t = (IsPrimitiveRoot.powerBasis K ⋯).equivOfMinpoly (IsPrimitiveRoot.powerBasis K ⋯) ⋯
• IsCyclotomicExtension.autEquivPow_apply 📋 Mathlib.NumberTheory.Cyclotomic.Gal
  {n : ℕ} [NeZero n] {K : Type u_1} [Field K] (L : Type u_2) [CommRing L] [IsDomain L] [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic n K)) (a✝ : L ≃ₐ[K] L) : (IsCyclotomicExtension.autEquivPow L h) a✝ = (↑(IsPrimitiveRoot.autToPow K ⋯)).toFun a✝
• galXPowEquivUnitsZMod 📋 Mathlib.NumberTheory.Cyclotomic.Gal
  {n : ℕ} [NeZero n] {K : Type u_1} [Field K] {L : Type u_2} [Field L] [Algebra K L] [IsCyclotomicExtension {n} K L] (h : Irreducible (Polynomial.cyclotomic n K)) : (Polynomial.X ^ n - 1).Gal ≃* (ZMod n)ˣ
• IsCyclotomicExtension.Rat.isTotallyComplex 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
  {n : ℕ} [NeZero n] (K : Type u) [Field K] [CharZero K] [IsCyclotomicExtension {n} ℚ K] (hn : 2 < n) : NumberField.IsTotallyComplex K
• IsCyclotomicExtension.Rat.nrComplexPlaces_eq_totient_div_two 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
  (n : ℕ) [NeZero n] (K : Type u) [Field K] [CharZero K] [h : IsCyclotomicExtension {n} ℚ K] : NumberField.InfinitePlace.nrComplexPlaces K = n.totient / 2
• IsCyclotomicExtension.Rat.nrRealPlaces_eq_zero 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
  {n : ℕ} [NeZero n] (K : Type u) [Field K] [CharZero K] [IsCyclotomicExtension {n} ℚ K] (hn : 2 < n) : NumberField.InfinitePlace.nrRealPlaces K = 0
• IsCyclotomicExtension.Rat.torsionOrder_eq 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {n : ℕ} {K : Type u} [Field K] [NeZero n] [NumberField K] [hK : IsCyclotomicExtension {n} ℚ K] : NumberField.Units.torsionOrder K = if Even n then n else 2 * n
• IsCyclotomicExtension.ringOfIntegers 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {n : ℕ} {K : Type u} [Field K] [NeZero n] [CharZero K] [IsCyclotomicExtension {n} ℚ K] : IsCyclotomicExtension {n} ℤ (NumberField.RingOfIntegers K)
• IsPrimitiveRoot.integralPowerBasis 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {n : ℕ} {K : Type u} [Field K] {ζ : K} [NeZero n] [CharZero K] [IsCyclotomicExtension {n} ℚ K] (hζ : IsPrimitiveRoot ζ n) : PowerBasis ℤ (NumberField.RingOfIntegers K)
• IsPrimitiveRoot.subOneIntegralPowerBasis 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {n : ℕ} {K : Type u} [Field K] {ζ : K} [NeZero n] [CharZero K] [IsCyclotomicExtension {n} ℚ K] (hζ : IsPrimitiveRoot ζ n) : PowerBasis ℤ (NumberField.RingOfIntegers K)
• IsCyclotomicExtension.Rat.finrank 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  (k : ℕ) (K : Type u) [Field K] [CharZero K] [NeZero k] [IsCyclotomicExtension {k} ℚ K] : Module.finrank ℚ K = k.totient
• IsPrimitiveRoot.integralPowerBasis_dim 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {n : ℕ} {K : Type u} [Field K] {ζ : K} [NeZero n] [CharZero K] [IsCyclotomicExtension {n} ℚ K] (hζ : IsPrimitiveRoot ζ n) : hζ.integralPowerBasis.dim = n.totient
• IsPrimitiveRoot.IsCyclotomicExtension.ringOfIntegersOfPrimePow 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ k} ℚ K] : IsCyclotomicExtension {p ^ k} ℤ (NumberField.RingOfIntegers K)
• IsPrimitiveRoot.integralPowerBasis_gen 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {n : ℕ} {K : Type u} [Field K] {ζ : K} [NeZero n] [CharZero K] [hcycl : IsCyclotomicExtension {n} ℚ K] (hζ : IsPrimitiveRoot ζ n) : hζ.integralPowerBasis.gen = hζ.toInteger
• IsPrimitiveRoot.integralPowerBasisOfPrimePow 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)) : PowerBasis ℤ (NumberField.RingOfIntegers K)
• IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)) : PowerBasis ℤ (NumberField.RingOfIntegers K)
• IsPrimitiveRoot.integralPowerBasisOfPrimePow_dim 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)) : hζ.integralPowerBasisOfPrimePow.dim = (p ^ k).totient
• IsCyclotomicExtension.Rat.natAbs_discr 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  (n : ℕ) (K : Type u) [Field K] [CharZero K] [hn : NeZero n] [hK : IsCyclotomicExtension {n} ℚ K] : (NumberField.discr K).natAbs = n ^ n.totient / ∏ p ∈ n.primeFactors, p ^ (n.totient / (p - 1))
• IsPrimitiveRoot.zeta_sub_one_prime' 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [h : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) : Prime (hζ.toInteger - 1)
• IsPrimitiveRoot.integralPowerBasisOfPrimePow_gen 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)) : hζ.integralPowerBasisOfPrimePow.gen = hζ.toInteger
• IsCyclotomicExtension.Rat.discr_prime 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  (p : ℕ) (K : Type u) [Field K] [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p} ℚ K] : NumberField.discr K = (-1) ^ ((p - 1) / 2) * ↑p ^ (p - 2)
• IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen_prime 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) : Prime hζ.subOneIntegralPowerBasisOfPrimePow.gen
• IsPrimitiveRoot.finite_quotient_span_sub_one' 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) : Finite (NumberField.RingOfIntegers K ⧸ Ideal.span {hζ.toInteger - 1})
• IsPrimitiveRoot.toInteger_sub_one_dvd_prime' 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) : hζ.toInteger - 1 ∣ ↑p
• IsCyclotomicExtension.Rat.discr 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  (n : ℕ) (K : Type u) [Field K] [CharZero K] [hn : NeZero n] [hK : IsCyclotomicExtension {n} ℚ K] : NumberField.discr K = (-1) ^ (n.totient / 2) * (↑n ^ n.totient / ↑(∏ p ∈ n.primeFactors, p ^ (n.totient / (p - 1))))
• IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two' 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) (hodd : p ≠ 2) : ¬∃ n, ↑p ∣ hζ.toInteger - ↑n
• IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) : IsIntegralClosure ↥ℤ[ζ] ℤ K
• IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {n : ℕ} {K : Type u} [Field K] [CharZero K] [hn : NeZero n] {ζ : K} [hcycl : IsCyclotomicExtension {n} ℚ K] (hζ : IsPrimitiveRoot ζ n) : IsIntegralClosure ↥ℤ[ζ] ℤ K
• IsPrimitiveRoot.zeta_sub_one_prime 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) : Prime (hζ.toInteger - 1)
• IsPrimitiveRoot.zeta_sub_one_prime_of_two_pow 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {k : ℕ} {K : Type u} [Field K] {ζ : K} [CharZero K] [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) : Prime (hζ.toInteger - 1)
• IsPrimitiveRoot.zeta_sub_one_prime_of_ne_two 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hodd : p ≠ 2) : Prime (hζ.toInteger - 1)
• IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)) : IsIntegralClosure ↥ℤ[ζ] ℤ K
• IsPrimitiveRoot.adjoinEquivRingOfIntegers 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {n : ℕ} {K : Type u} [Field K] {ζ : K} [NeZero n] [CharZero K] [IsCyclotomicExtension {n} ℚ K] (hζ : IsPrimitiveRoot ζ n) : ↥ℤ[ζ] ≃ₐ[ℤ] NumberField.RingOfIntegers K
• IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {K : Type u} [Field K] {ζ : K} [CharZero K] [IsCyclotomicExtension {2} ℚ K] (hζ : IsPrimitiveRoot ζ 2) : (Algebra.norm ℤ) (hζ.toInteger - 1) = -2
• IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two' 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) (hodd : p ≠ 2) : Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))
• IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two' 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) (h : p ≠ 2) : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑p
• IsCyclotomicExtension.Rat.discr_prime_pow 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  (p k : ℕ) (K : Type u) [Field K] [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ k} ℚ K] : NumberField.discr K = (-1) ^ ((p ^ k).totient / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
• IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)) : ↥ℤ[ζ] ≃ₐ[ℤ] NumberField.RingOfIntegers K
• IsPrimitiveRoot.finite_quotient_span_sub_one 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) : Finite (NumberField.RingOfIntegers K ⧸ Ideal.span {hζ.toInteger - 1})
• IsPrimitiveRoot.toInteger_sub_one_dvd_prime 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) : hζ.toInteger - 1 ∣ ↑p
• IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hodd : p ≠ 2) : ¬∃ n, ↑p ∣ hζ.toInteger - ↑n
• IsPrimitiveRoot.norm_toInteger_sub_one_eq_one 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {K : Type u} [Field K] {ζ : K} [CharZero K] {n : ℕ} [IsCyclotomicExtension {n} ℚ K] (hζ : IsPrimitiveRoot ζ n) (h₁ : 2 < n) (h₂ : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n) : have this := ⋯; (Algebra.norm ℤ) (hζ.toInteger - 1) = 1
• IsPrimitiveRoot.toInteger_sub_one_not_dvd_two 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hodd : p ≠ 2) : ¬hζ.toInteger - 1 ∣ 2
• IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_pow_ne_two 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (htwo : p ^ (k + 1) ≠ 2) : ¬∃ n, ↑p ∣ hζ.toInteger - ↑n
• IsPrimitiveRoot.subOneIntegralPowerBasis_gen 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {n : ℕ} {K : Type u} [Field K] {ζ : K} [NeZero n] [CharZero K] [IsCyclotomicExtension {n} ℚ K] (hζ : IsPrimitiveRoot ζ n) : hζ.subOneIntegralPowerBasis.gen = ⟨ζ - 1, ⋯⟩
• IsCyclotomicExtension.Rat.discr_prime_pow_succ 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  (p k : ℕ) (K : Type u) [Field K] [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] : NumberField.discr K = (-1) ^ (p ^ k * (p - 1) / 2) * ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
• IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two_pow 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {k : ℕ} {K : Type u_1} [Field K] {ζ : K} [CharZero K] [IsCyclotomicExtension {2 ^ (k + 2)} ℚ K] (hζ : IsPrimitiveRoot ζ (2 ^ (k + 2))) : (Algebra.norm ℤ) (hζ.toInteger - 1) = 2
• IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hodd : p ≠ 2) : Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))
• IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hodd : p ≠ 2) : (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑p
• IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_pow_ne_two 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (htwo : p ^ (k + 1) ≠ 2) : Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))
• IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)) : hζ.subOneIntegralPowerBasisOfPrimePow.gen = ⟨ζ - 1, ⋯⟩
• IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_ne_two 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) {s : ℕ} (hs : s ≤ k) (hodd : p ≠ 2) : (Algebra.norm ℤ) (hζ.toInteger ^ p ^ s - 1) = ↑p ^ p ^ s
• IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_two 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {k : ℕ} {K : Type u} [Field K] {ζ : K} [CharZero K] [IsCyclotomicExtension {2 ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))) : (Algebra.norm ℤ) (hζ.toInteger ^ 2 ^ k - 1) = (-2) ^ 2 ^ k
• IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_pow_ne_two 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) {s : ℕ} (hs : s ≤ k) (htwo : p ^ (k - s + 1) ≠ 2) : (Algebra.norm ℤ) (hζ.toInteger ^ p ^ s - 1) = ↑p ^ p ^ s
• IsCyclotomicExtension.Rat.adjoin_singleton_eq_top 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {n : ℕ} {K : Type u} [Field K] [CharZero K] [hn : NeZero n] [hK : IsCyclotomicExtension {n} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ n) : ℤ[hζ.toInteger] = ⊤
• IsCyclotomicExtension.Rat.discr_odd_prime' 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) (hodd : p ≠ 2) : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = (-1) ^ ((p - 1) / 2) * ↑p ^ (p - 2)
• IsCyclotomicExtension.Rat.discr_prime_pow_eq_unit_mul_pow' 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)) : ∃ u n, Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = ↑↑u * ↑p ^ n
• IsCyclotomicExtension.Rat.discr_prime_pow' 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)) : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = (-1) ^ ((p ^ k).totient / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
• IsCyclotomicExtension.Rat.discr_prime_pow_ne_two' 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))) (hk : p ^ (k + 1) ≠ 2) : Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis = (-1) ^ ((p ^ (k + 1)).totient / 2) * ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
• IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {n : ℕ} {K : Type u} [Field K] {ζ : K} [NeZero n] [CharZero K] [IsCyclotomicExtension {n} ℚ K] (hζ : IsPrimitiveRoot ζ n) (a : NumberField.RingOfIntegers K) : hζ.adjoinEquivRingOfIntegers.symm a = (IsIntegralClosure.lift ℤ (↥ℤ[ζ]) K) a
• IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_symm_apply 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)) (a : NumberField.RingOfIntegers K) : hζ.adjoinEquivRingOfIntegersOfPrimePow.symm a = (IsIntegralClosure.lift ℤ (↥ℤ[ζ]) K) a
• IsPrimitiveRoot.adjoinEquivRingOfIntegers_apply 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {n : ℕ} {K : Type u} [Field K] {ζ : K} [NeZero n] [CharZero K] [IsCyclotomicExtension {n} ℚ K] (hζ : IsPrimitiveRoot ζ n) (a : ↥ℤ[ζ]) : hζ.adjoinEquivRingOfIntegers a = (IsIntegralClosure.lift ℤ (NumberField.RingOfIntegers K) K) a
• IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_apply 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
  {p k : ℕ} {K : Type u} [Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [CharZero K] [IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)) (a : ↥ℤ[ζ]) : hζ.adjoinEquivRingOfIntegersOfPrimePow a = (IsIntegralClosure.lift ℤ (NumberField.RingOfIntegers K) K) a
• IsCyclotomicExtension.Rat.five_pid 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.PID
  (K : Type u) [Field K] [NumberField K] [IsCyclotomicExtension {5} ℚ K] : IsPrincipalIdealRing (NumberField.RingOfIntegers K)
• IsCyclotomicExtension.Rat.three_pid 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.PID
  (K : Type u) [Field K] [NumberField K] [IsCyclotomicExtension {3} ℚ K] : IsPrincipalIdealRing (NumberField.RingOfIntegers K)
• IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_add_one_of_dvd_add_one 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Three
  {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) [NumberField K] [IsCyclotomicExtension {3} ℚ K] {x : NumberField.RingOfIntegers K} (h : hζ.toInteger - 1 ∣ x + 1) : (hζ.toInteger - 1) ^ 4 ∣ x ^ 3 + 1
• IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_of_dvd_sub_one 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Three
  {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) [NumberField K] [IsCyclotomicExtension {3} ℚ K] {x : NumberField.RingOfIntegers K} (h : hζ.toInteger - 1 ∣ x - 1) : (hζ.toInteger - 1) ^ 4 ∣ x ^ 3 - 1
• IsCyclotomicExtension.Rat.Three.lambda_dvd_mul_sub_one_mul_sub_eta_add_one 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Three
  {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) (x : NumberField.RingOfIntegers K) [NumberField K] [IsCyclotomicExtension {3} ℚ K] : hζ.toInteger - 1 ∣ x * (x - 1) * (x - (↑⋯.unit + 1))
• IsCyclotomicExtension.Rat.Three.lambda_dvd_or_dvd_sub_one_or_dvd_add_one 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Three
  {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) (x : NumberField.RingOfIntegers K) [NumberField K] [IsCyclotomicExtension {3} ℚ K] : hζ.toInteger - 1 ∣ x ∨ hζ.toInteger - 1 ∣ x - 1 ∨ hζ.toInteger - 1 ∣ x + 1
• IsCyclotomicExtension.Rat.Three.eq_one_or_neg_one_of_unit_of_congruent 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Three
  {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) (u : (NumberField.RingOfIntegers K)ˣ) [NumberField K] [IsCyclotomicExtension {3} ℚ K] (hcong : ∃ n, (hζ.toInteger - 1) ^ 2 ∣ ↑u - ↑n) : u = 1 ∨ u = -1
• IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Three
  {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) [NumberField K] [IsCyclotomicExtension {3} ℚ K] {x : NumberField.RingOfIntegers K} (h : ¬hζ.toInteger - 1 ∣ x) : (hζ.toInteger - 1) ^ 4 ∣ x ^ 3 - 1 ∨ (hζ.toInteger - 1) ^ 4 ∣ x ^ 3 + 1
• IsCyclotomicExtension.Rat.Three.Units.mem 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Three
  {K : Type u_1} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) (u : (NumberField.RingOfIntegers K)ˣ) [NumberField K] [IsCyclotomicExtension {3} ℚ K] : u ∈ [1, -1, ⋯.unit, -⋯.unit, ⋯.unit ^ 2, -⋯.unit ^ 2]
• IsCyclotomicExtension.Rat.instIsCMFieldOfTopSetNatRat 📋 Mathlib.NumberTheory.NumberField.CMField
  (K : Type u_1) [Field K] [CharZero K] [IsCyclotomicExtension ⊤ ℚ K] : NumberField.IsCMField K
• IsCyclotomicExtension.Rat.isCMField 📋 Mathlib.NumberTheory.NumberField.CMField
  (K : Type u_1) [Field K] [CharZero K] {S : Set ℕ} (hS : ∃ n ∈ S, 2 < n) [IsCyclotomicExtension S ℚ K] : NumberField.IsCMField K
• IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
  (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {p} ℚ K] : (Ideal.span {↑p}).inertiaDegIn (NumberField.RingOfIntegers K) = 1
• IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
  (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {p} ℚ K] : (Ideal.span {↑p}).ramificationIdxIn (NumberField.RingOfIntegers K) = p - 1
• IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_not_dvd 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
  {m : ℕ} (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [NeZero m] [hK : IsCyclotomicExtension {m} ℚ K] (hm : ¬p ∣ m) : (Ideal.span {↑p}).ramificationIdxIn (NumberField.RingOfIntegers K) = 1
• IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime_pow 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
  (p k : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] : (Ideal.span {↑p}).inertiaDegIn (NumberField.RingOfIntegers K) = 1
• IsCyclotomicExtension.Rat.ncard_primesOver_of_prime 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
  (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {p} ℚ K] : ((Ideal.span {↑p}).primesOver (NumberField.RingOfIntegers K)).ncard = 1
• IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_not_dvd 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
  {m : ℕ} (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [NeZero m] [hK : IsCyclotomicExtension {m} ℚ K] (hm : ¬p ∣ m) : (Ideal.span {↑p}).inertiaDegIn (NumberField.RingOfIntegers K) = orderOf ↑p
• IsCyclotomicExtension.Rat.ncard_primesOver_of_prime_pow 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
  (p k : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] : ((Ideal.span {↑p}).primesOver (NumberField.RingOfIntegers K)).ncard = 1
• IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime_pow 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
  (p k : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] : (Ideal.span {↑p}).ramificationIdxIn (NumberField.RingOfIntegers K) = p ^ k * (p - 1)
• IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
  (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {p} ℚ K] (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver (Ideal.span {↑p})] : P.inertiaDeg ℤ = 1
• IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
  (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {p} ℚ K] (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver (Ideal.span {↑p})] : P.ramificationIdx ℤ = p - 1
• IsCyclotomicExtension.Rat.inertiaDegIn_eq 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
  (n : ℕ) {m p k : ℕ} [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {n} ℚ K] (hn : n = p ^ (k + 1) * m) (hm : ¬p ∣ m) : (Ideal.span {↑p}).inertiaDegIn (NumberField.RingOfIntegers K) = orderOf ↑p
• IsCyclotomicExtension.Rat.ramificationIdxIn_eq 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
  (n : ℕ) {m p k : ℕ} [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [IsCyclotomicExtension {n} ℚ K] (hn : n = p ^ (k + 1) * m) (hm : ¬p ∣ m) : (Ideal.span {↑p}).ramificationIdxIn (NumberField.RingOfIntegers K) = p ^ k * (p - 1)
• IsCyclotomicExtension.Rat.ramificationIdx_eq_of_not_dvd 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
  {m : ℕ} (p : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver (Ideal.span {↑p})] [NeZero m] [hK : IsCyclotomicExtension {m} ℚ K] (hm : ¬p ∣ m) : P.ramificationIdx ℤ = 1
• IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime_pow 📋 Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
  (p k : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [Field K] [NumberField K] [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (P : Ideal (NumberField.RingOfIntegers K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver (Ideal.span {↑p})] : P.inertiaDeg ℤ = 1

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59