[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ IsCyclotomicExtension {n} A B ↔ (∃ r, IsPrimitiveRoot r ↑n) ∧ ∀ (x : B), x ∈ adjoin A {b | b ^ ↑n = 1}
[PROOFSTEP]
simp [IsCyclotomicExtension_iff]
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : IsCyclotomicExtension ∅ A B
⊢ ⊥ = ⊤
[PROOFSTEP]
simpa [Algebra.eq_top_iff, IsCyclotomicExtension_iff] using h
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : IsCyclotomicExtension {1} A B
x : B
⊢ x ∈ ⊥
[PROOFSTEP]
simpa [adjoin_singleton_one] using ((IsCyclotomicExtension_iff _ _ _).1 h).2 x
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ⊥ = ⊤
⊢ IsCyclotomicExtension ∅ A B
[PROOFSTEP]
refine' (iff_adjoin_eq_top _ A _).2 ⟨fun s hs => by simp at hs , _root_.eq_top_iff.2 fun x hx => _⟩
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ⊥ = ⊤
s : ℕ+
hs : s ∈ ∅
⊢ ∃ r, IsPrimitiveRoot r ↑s
[PROOFSTEP]
simp at hs 
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ⊥ = ⊤
x : B
hx : x ∈ ⊤
⊢ x ∈ adjoin A {b | ∃ n, n ∈ ∅ ∧ b ^ ↑n = 1}
[PROOFSTEP]
rw [← h] at hx 
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ⊥ = ⊤
x : B
hx : x ∈ ⊥
⊢ x ∈ adjoin A {b | ∃ n, n ∈ ∅ ∧ b ^ ↑n = 1}
[PROOFSTEP]
simpa using hx
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : 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
[PROOFSTEP]
refine' ⟨fun hn => _, fun x => _⟩
[GOAL]
case refine'_1
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ↑(algebraMap B C)
n✝ : ℕ+
hn : n✝ ∈ S ∪ T
⊢ ∃ r, IsPrimitiveRoot r ↑n✝
[PROOFSTEP]
cases' hn with hn hn
[GOAL]
case refine'_1.inl
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ↑(algebraMap B C)
n✝ : ℕ+
hn : n✝ ∈ S
⊢ ∃ r, IsPrimitiveRoot r ↑n✝
[PROOFSTEP]
obtain ⟨b, hb⟩ := ((IsCyclotomicExtension_iff _ _ _).1 hS).1 hn
[GOAL]
case refine'_1.inl.intro
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ↑(algebraMap B C)
n✝ : ℕ+
hn : n✝ ∈ S
b : B
hb : IsPrimitiveRoot b ↑n✝
⊢ ∃ r, IsPrimitiveRoot r ↑n✝
[PROOFSTEP]
refine' ⟨algebraMap B C b, _⟩
[GOAL]
case refine'_1.inl.intro
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ↑(algebraMap B C)
n✝ : ℕ+
hn : n✝ ∈ S
b : B
hb : IsPrimitiveRoot b ↑n✝
⊢ IsPrimitiveRoot (↑(algebraMap B C) b) ↑n✝
[PROOFSTEP]
exact hb.map_of_injective h
[GOAL]
case refine'_1.inr
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ↑(algebraMap B C)
n✝ : ℕ+
hn : n✝ ∈ T
⊢ ∃ r, IsPrimitiveRoot r ↑n✝
[PROOFSTEP]
exact ((IsCyclotomicExtension_iff _ _ _).1 hT).1 hn
[GOAL]
case refine'_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ↑(algebraMap B C)
x : C
⊢ x ∈ adjoin A {b | ∃ n, n ∈ S ∪ T ∧ b ^ ↑n = 1}
[PROOFSTEP]
refine'
  adjoin_induction (((IsCyclotomicExtension_iff T B _).1 hT).2 x)
    (fun c ⟨n, hn⟩ => subset_adjoin ⟨n, Or.inr hn.1, hn.2⟩) (fun b => _) (fun x y hx hy => Subalgebra.add_mem _ hx hy)
    fun x y hx hy => Subalgebra.mul_mem _ hx hy
[GOAL]
case refine'_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ↑(algebraMap B C)
x : C
b : B
⊢ ↑(algebraMap B C) b ∈ adjoin A {b | ∃ n, n ∈ S ∪ T ∧ b ^ ↑n = 1}
[PROOFSTEP]
let f := IsScalarTower.toAlgHom A B C
[GOAL]
case refine'_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ↑(algebraMap B C)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
⊢ ↑(algebraMap B C) b ∈ adjoin A {b | ∃ n, n ∈ S ∪ T ∧ b ^ ↑n = 1}
[PROOFSTEP]
have hb : f b ∈ (adjoin A {b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1}).map f :=
  ⟨b, ((IsCyclotomicExtension_iff _ _ _).1 hS).2 b, rfl⟩
[GOAL]
case refine'_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ↑(algebraMap B C)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
hb : ↑f b ∈ Subalgebra.map f (adjoin A {b | ∃ a, a ∈ S ∧ b ^ ↑a = 1})
⊢ ↑(algebraMap B C) b ∈ adjoin A {b | ∃ n, n ∈ S ∪ T ∧ b ^ ↑n = 1}
[PROOFSTEP]
rw [IsScalarTower.toAlgHom_apply, ← adjoin_image] at hb 
[GOAL]
case refine'_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ↑(algebraMap B C)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
hb : ↑(algebraMap B C) b ∈ adjoin A (↑f '' {b | ∃ a, a ∈ S ∧ b ^ ↑a = 1})
⊢ ↑(algebraMap B C) b ∈ adjoin A {b | ∃ n, n ∈ S ∪ T ∧ b ^ ↑n = 1}
[PROOFSTEP]
refine' adjoin_mono (fun y hy => _) hb
[GOAL]
case refine'_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ↑(algebraMap B C)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
hb : ↑(algebraMap B C) b ∈ adjoin A (↑f '' {b | ∃ a, a ∈ S ∧ b ^ ↑a = 1})
y : C
hy : y ∈ ↑f '' {b | ∃ a, a ∈ S ∧ b ^ ↑a = 1}
⊢ y ∈ {b | ∃ n, n ∈ S ∪ T ∧ b ^ ↑n = 1}
[PROOFSTEP]
obtain ⟨b₁, ⟨⟨n, hn⟩, h₁⟩⟩ := hy
[GOAL]
case refine'_2.intro.intro.intro
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ↑(algebraMap B C)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
hb : ↑(algebraMap B C) b ∈ adjoin A (↑f '' {b | ∃ a, a ∈ S ∧ b ^ ↑a = 1})
y : C
b₁ : B
h₁ : ↑f b₁ = y
n : ℕ+
hn : n ∈ S ∧ b₁ ^ ↑n = 1
⊢ y ∈ {b | ∃ n, n ∈ S ∪ T ∧ b ^ ↑n = 1}
[PROOFSTEP]
exact ⟨n, ⟨mem_union_left T hn.1, by rw [← h₁, ← AlgHom.map_pow, hn.2, AlgHom.map_one]⟩⟩
[GOAL]
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
C : Type w
inst✝³ : CommRing C
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective ↑(algebraMap B C)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
hb : ↑(algebraMap B C) b ∈ adjoin A (↑f '' {b | ∃ a, a ∈ S ∧ b ^ ↑a = 1})
y : C
b₁ : B
h₁ : ↑f b₁ = y
n : ℕ+
hn : n ∈ S ∧ b₁ ^ ↑n = 1
⊢ y ^ ↑n = 1
[PROOFSTEP]
rw [← h₁, ← AlgHom.map_pow, hn.2, AlgHom.map_one]
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Subsingleton B
⊢ IsCyclotomicExtension S A B ↔ S = ∅ ∨ S = {1}
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Subsingleton B
⊢ IsCyclotomicExtension S A B → S = ∅ ∨ S = {1}
[PROOFSTEP]
rintro ⟨hprim, -⟩
[GOAL]
case mp.mk
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Subsingleton B
hprim : ∀ {n : ℕ+}, n ∈ S → ∃ r, IsPrimitiveRoot r ↑n
⊢ S = ∅ ∨ S = {1}
[PROOFSTEP]
rw [← subset_singleton_iff_eq]
[GOAL]
case mp.mk
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Subsingleton B
hprim : ∀ {n : ℕ+}, n ∈ S → ∃ r, IsPrimitiveRoot r ↑n
⊢ S ⊆ {1}
[PROOFSTEP]
intro t ht
[GOAL]
case mp.mk
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Subsingleton B
hprim : ∀ {n : ℕ+}, n ∈ S → ∃ r, IsPrimitiveRoot r ↑n
t : ℕ+
ht : t ∈ S
⊢ t ∈ {1}
[PROOFSTEP]
obtain ⟨ζ, hζ⟩ := hprim ht
[GOAL]
case mp.mk.intro
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Subsingleton B
hprim : ∀ {n : ℕ+}, n ∈ S → ∃ r, IsPrimitiveRoot r ↑n
t : ℕ+
ht : t ∈ S
ζ : B
hζ : IsPrimitiveRoot ζ ↑t
⊢ t ∈ {1}
[PROOFSTEP]
rw [mem_singleton_iff, ← PNat.coe_eq_one_iff]
[GOAL]
case mp.mk.intro
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Subsingleton B
hprim : ∀ {n : ℕ+}, n ∈ S → ∃ r, IsPrimitiveRoot r ↑n
t : ℕ+
ht : t ∈ S
ζ : B
hζ : IsPrimitiveRoot ζ ↑t
⊢ ↑t = 1
[PROOFSTEP]
exact_mod_cast hζ.unique (IsPrimitiveRoot.of_subsingleton ζ)
[GOAL]
case mpr
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Subsingleton B
⊢ S = ∅ ∨ S = {1} → IsCyclotomicExtension S A B
[PROOFSTEP]
rintro
  (rfl | rfl)
      -- Porting note: `R := A` was not needed.
[GOAL]
case mpr.inl
n : ℕ+
T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Subsingleton B
⊢ IsCyclotomicExtension ∅ A B
[PROOFSTEP]
exact ⟨fun h => h.elim, fun x => by convert (mem_top (R := A) : x ∈ ⊤)⟩
[GOAL]
n : ℕ+
T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Subsingleton B
x : B
⊢ x ∈ adjoin A {b | ∃ n, n ∈ ∅ ∧ b ^ ↑n = 1}
[PROOFSTEP]
convert (mem_top (R := A) : x ∈ ⊤)
[GOAL]
case mpr.inr
n : ℕ+
T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Subsingleton B
⊢ IsCyclotomicExtension {1} A B
[PROOFSTEP]
rw [iff_singleton]
[GOAL]
case mpr.inr
n : ℕ+
T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Subsingleton B
⊢ (∃ r, IsPrimitiveRoot r ↑1) ∧ ∀ (x : B), x ∈ adjoin A {b | b ^ ↑1 = 1}
[PROOFSTEP]
exact ⟨⟨0, IsPrimitiveRoot.of_subsingleton 0⟩, fun x => by convert (mem_top (R := A) : x ∈ ⊤)⟩
[GOAL]
n : ℕ+
T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Subsingleton B
x : B
⊢ x ∈ adjoin A {b | b ^ ↑1 = 1}
[PROOFSTEP]
convert (mem_top (R := A) : x ∈ ⊤)
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : IsCyclotomicExtension (S ∪ T) A B
⊢ IsCyclotomicExtension T { x // x ∈ adjoin A {b | ∃ a, a ∈ S ∧ b ^ ↑a = 1} } B
[PROOFSTEP]
have :
  {b : B | ∃ n : ℕ+, n ∈ S ∪ T ∧ b ^ (n : ℕ) = 1} =
    {b : B | ∃ n : ℕ+, n ∈ S ∧ b ^ (n : ℕ) = 1} ∪ {b : B | ∃ n : ℕ+, n ∈ T ∧ b ^ (n : ℕ) = 1} :=
  by
  refine' le_antisymm _ _
  · rintro x ⟨n, hn₁ | hn₂, hnpow⟩
    · left; exact ⟨n, hn₁, hnpow⟩
    · right; exact ⟨n, hn₂, hnpow⟩
  · rintro x (⟨n, hn⟩ | ⟨n, hn⟩)
    · exact ⟨n, Or.inl hn.1, hn.2⟩
    · exact ⟨n, Or.inr hn.1, hn.2⟩
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : IsCyclotomicExtension (S ∪ T) A B
⊢ {b | ∃ n, n ∈ S ∪ T ∧ b ^ ↑n = 1} = {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} ∪ {b | ∃ n, n ∈ T ∧ b ^ ↑n = 1}
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : IsCyclotomicExtension (S ∪ T) A B
⊢ {b | ∃ n, n ∈ S ∪ T ∧ b ^ ↑n = 1} ≤ {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} ∪ {b | ∃ n, n ∈ T ∧ b ^ ↑n = 1}
[PROOFSTEP]
rintro x ⟨n, hn₁ | hn₂, hnpow⟩
[GOAL]
case refine'_1.intro.intro.inl
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ+
hnpow : x ^ ↑n = 1
hn₁ : n ∈ S
⊢ x ∈ {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} ∪ {b | ∃ n, n ∈ T ∧ b ^ ↑n = 1}
[PROOFSTEP]
left
[GOAL]
case refine'_1.intro.intro.inl.h
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ+
hnpow : x ^ ↑n = 1
hn₁ : n ∈ S
⊢ x ∈ {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1}
[PROOFSTEP]
exact ⟨n, hn₁, hnpow⟩
[GOAL]
case refine'_1.intro.intro.inr
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ+
hnpow : x ^ ↑n = 1
hn₂ : n ∈ T
⊢ x ∈ {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} ∪ {b | ∃ n, n ∈ T ∧ b ^ ↑n = 1}
[PROOFSTEP]
right
[GOAL]
case refine'_1.intro.intro.inr.h
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ+
hnpow : x ^ ↑n = 1
hn₂ : n ∈ T
⊢ x ∈ {b | ∃ n, n ∈ T ∧ b ^ ↑n = 1}
[PROOFSTEP]
exact ⟨n, hn₂, hnpow⟩
[GOAL]
case refine'_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : IsCyclotomicExtension (S ∪ T) A B
⊢ {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} ∪ {b | ∃ n, n ∈ T ∧ b ^ ↑n = 1} ≤ {b | ∃ n, n ∈ S ∪ T ∧ b ^ ↑n = 1}
[PROOFSTEP]
rintro x (⟨n, hn⟩ | ⟨n, hn⟩)
[GOAL]
case refine'_2.inl.intro
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ+
hn : n ∈ S ∧ x ^ ↑n = 1
⊢ x ∈ {b | ∃ n, n ∈ S ∪ T ∧ b ^ ↑n = 1}
[PROOFSTEP]
exact ⟨n, Or.inl hn.1, hn.2⟩
[GOAL]
case refine'_2.inr.intro
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ+
hn : n ∈ T ∧ x ^ ↑n = 1
⊢ x ∈ {b | ∃ n, n ∈ S ∪ T ∧ b ^ ↑n = 1}
[PROOFSTEP]
exact ⟨n, Or.inr hn.1, hn.2⟩
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : IsCyclotomicExtension (S ∪ T) A B
this : {b | ∃ n, n ∈ S ∪ T ∧ b ^ ↑n = 1} = {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} ∪ {b | ∃ n, n ∈ T ∧ b ^ ↑n = 1}
⊢ IsCyclotomicExtension T { x // x ∈ adjoin A {b | ∃ a, a ∈ S ∧ b ^ ↑a = 1} } B
[PROOFSTEP]
refine' ⟨fun hn => ((IsCyclotomicExtension_iff _ A _).1 h).1 (mem_union_right S hn), fun b => _⟩
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : IsCyclotomicExtension (S ∪ T) A B
this : {b | ∃ n, n ∈ S ∪ T ∧ b ^ ↑n = 1} = {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} ∪ {b | ∃ n, n ∈ T ∧ b ^ ↑n = 1}
b : B
⊢ b ∈ adjoin { x // x ∈ adjoin A {b | ∃ a, a ∈ S ∧ b ^ ↑a = 1} } {b | ∃ n, n ∈ T ∧ b ^ ↑n = 1}
[PROOFSTEP]
replace h := ((IsCyclotomicExtension_iff _ _ _).1 h).2 b
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
this : {b | ∃ n, n ∈ S ∪ T ∧ b ^ ↑n = 1} = {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} ∪ {b | ∃ n, n ∈ T ∧ b ^ ↑n = 1}
b : B
h : b ∈ adjoin A {b | ∃ n, n ∈ S ∪ T ∧ b ^ ↑n = 1}
⊢ b ∈ adjoin { x // x ∈ adjoin A {b | ∃ a, a ∈ S ∧ b ^ ↑a = 1} } {b | ∃ n, n ∈ T ∧ b ^ ↑n = 1}
[PROOFSTEP]
rwa [this, adjoin_union_eq_adjoin_adjoin, Subalgebra.mem_restrictScalars] at h 
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : IsCyclotomicExtension T A B
hS : S ⊆ T
⊢ IsCyclotomicExtension S A { x // x ∈ adjoin A {b | ∃ a, a ∈ S ∧ b ^ ↑a = 1} }
[PROOFSTEP]
refine' ⟨@fun n hn => _, fun b => _⟩
[GOAL]
case refine'_1
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : IsCyclotomicExtension T A B
hS : S ⊆ T
n : ℕ+
hn : n ∈ S
⊢ ∃ r, IsPrimitiveRoot r ↑n
[PROOFSTEP]
obtain ⟨b, hb⟩ := ((IsCyclotomicExtension_iff _ _ _).1 h).1 (hS hn)
[GOAL]
case refine'_1.intro
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : IsCyclotomicExtension T A B
hS : S ⊆ T
n : ℕ+
hn : n ∈ S
b : B
hb : IsPrimitiveRoot b ↑n
⊢ ∃ r, IsPrimitiveRoot r ↑n
[PROOFSTEP]
refine' ⟨⟨b, subset_adjoin ⟨n, hn, hb.pow_eq_one⟩⟩, _⟩
[GOAL]
case refine'_1.intro
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : IsCyclotomicExtension T A B
hS : S ⊆ T
n : ℕ+
hn : n ∈ S
b : B
hb : IsPrimitiveRoot b ↑n
⊢ IsPrimitiveRoot { val := b, property := (_ : b ∈ ↑(adjoin A {b | ∃ a, a ∈ S ∧ b ^ ↑a = 1})) } ↑n
[PROOFSTEP]
rwa [← IsPrimitiveRoot.coe_submonoidClass_iff, Subtype.coe_mk]
[GOAL]
case refine'_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : IsCyclotomicExtension T A B
hS : S ⊆ T
b : { x // x ∈ adjoin A {b | ∃ a, a ∈ S ∧ b ^ ↑a = 1} }
⊢ b ∈ adjoin A {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1}
[PROOFSTEP]
convert mem_top (R := A) (x := b)
[GOAL]
case h.e'_5
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : IsCyclotomicExtension T A B
hS : S ⊆ T
b : { x // x ∈ adjoin A {b | ∃ a, a ∈ S ∧ b ^ ↑a = 1} }
⊢ adjoin A {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} = ⊤
[PROOFSTEP]
rw [← adjoin_adjoin_coe_preimage, preimage_setOf_eq]
[GOAL]
case h.e'_5
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : IsCyclotomicExtension T A B
hS : S ⊆ T
b : { x // x ∈ adjoin A {b | ∃ a, a ∈ S ∧ b ^ ↑a = 1} }
⊢ adjoin A {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} = adjoin A {a | ∃ a_1, a_1 ∈ S ∧ ↑a ^ ↑a_1 = 1}
[PROOFSTEP]
norm_cast
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ (s : ℕ+), s ∈ S → n ∣ s
hS : Set.Nonempty S
H : IsCyclotomicExtension S A B
⊢ IsCyclotomicExtension (S ∪ {n}) A B
[PROOFSTEP]
refine' (iff_adjoin_eq_top _ A _).2 ⟨fun s hs => _, _⟩
[GOAL]
case refine'_1
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ (s : ℕ+), s ∈ S → n ∣ s
hS : Set.Nonempty S
H : IsCyclotomicExtension S A B
s : ℕ+
hs : s ∈ S ∪ {n}
⊢ ∃ r, IsPrimitiveRoot r ↑s
[PROOFSTEP]
rw [mem_union, mem_singleton_iff] at hs 
[GOAL]
case refine'_1
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ (s : ℕ+), s ∈ S → n ∣ s
hS : Set.Nonempty S
H : IsCyclotomicExtension S A B
s : ℕ+
hs : s ∈ S ∨ s = n
⊢ ∃ r, IsPrimitiveRoot r ↑s
[PROOFSTEP]
obtain hs | rfl := hs
[GOAL]
case refine'_1.inl
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ (s : ℕ+), s ∈ S → n ∣ s
hS : Set.Nonempty S
H : IsCyclotomicExtension S A B
s : ℕ+
hs : s ∈ S
⊢ ∃ r, IsPrimitiveRoot r ↑s
[PROOFSTEP]
exact H.exists_prim_root hs
[GOAL]
case refine'_1.inr
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hS : Set.Nonempty S
H : IsCyclotomicExtension S A B
s : ℕ+
h : ∀ (s_1 : ℕ+), s_1 ∈ S → s ∣ s_1
⊢ ∃ r, IsPrimitiveRoot r ↑s
[PROOFSTEP]
obtain ⟨m, hm⟩ := hS
[GOAL]
case refine'_1.inr.intro
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension S A B
s : ℕ+
h : ∀ (s_1 : ℕ+), s_1 ∈ S → s ∣ s_1
m : ℕ+
hm : m ∈ S
⊢ ∃ r, IsPrimitiveRoot r ↑s
[PROOFSTEP]
obtain ⟨x, rfl⟩ := h m hm
[GOAL]
case refine'_1.inr.intro.intro
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension S A B
s : ℕ+
h : ∀ (s_1 : ℕ+), s_1 ∈ S → s ∣ s_1
x : ℕ+
hm : s * x ∈ S
⊢ ∃ r, IsPrimitiveRoot r ↑s
[PROOFSTEP]
obtain ⟨ζ, hζ⟩ := H.exists_prim_root hm
[GOAL]
case refine'_1.inr.intro.intro.intro
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension S A B
s : ℕ+
h : ∀ (s_1 : ℕ+), s_1 ∈ S → s ∣ s_1
x : ℕ+
hm : s * x ∈ S
ζ : B
hζ : IsPrimitiveRoot ζ ↑(s * x)
⊢ ∃ r, IsPrimitiveRoot r ↑s
[PROOFSTEP]
refine' ⟨ζ ^ (x : ℕ), _⟩
[GOAL]
case refine'_1.inr.intro.intro.intro
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension S A B
s : ℕ+
h : ∀ (s_1 : ℕ+), s_1 ∈ S → s ∣ s_1
x : ℕ+
hm : s * x ∈ S
ζ : B
hζ : IsPrimitiveRoot ζ ↑(s * x)
⊢ IsPrimitiveRoot (ζ ^ ↑x) ↑s
[PROOFSTEP]
convert hζ.pow_of_dvd x.ne_zero (dvd_mul_left (x : ℕ) s)
[GOAL]
case h.e'_4
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension S A B
s : ℕ+
h : ∀ (s_1 : ℕ+), s_1 ∈ S → s ∣ s_1
x : ℕ+
hm : s * x ∈ S
ζ : B
hζ : IsPrimitiveRoot ζ ↑(s * x)
⊢ ↑s = ↑(s * x) / ↑x
[PROOFSTEP]
simp only [PNat.mul_coe, Nat.mul_div_left, PNat.pos]
[GOAL]
case refine'_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ (s : ℕ+), s ∈ S → n ∣ s
hS : Set.Nonempty S
H : IsCyclotomicExtension S A B
⊢ adjoin A {b | ∃ n_1, n_1 ∈ S ∪ {n} ∧ b ^ ↑n_1 = 1} = ⊤
[PROOFSTEP]
refine' _root_.eq_top_iff.2 _
[GOAL]
case refine'_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ (s : ℕ+), s ∈ S → n ∣ s
hS : Set.Nonempty S
H : IsCyclotomicExtension S A B
⊢ ⊤ ≤ adjoin A {b | ∃ n_1, n_1 ∈ S ∪ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
rw [← ((iff_adjoin_eq_top S A B).1 H).2]
[GOAL]
case refine'_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ (s : ℕ+), s ∈ S → n ∣ s
hS : Set.Nonempty S
H : IsCyclotomicExtension S A B
⊢ adjoin A {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} ≤ adjoin A {b | ∃ n_1, n_1 ∈ S ∪ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
refine' adjoin_mono fun x hx => _
[GOAL]
case refine'_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ (s : ℕ+), s ∈ S → n ∣ s
hS : Set.Nonempty S
H : IsCyclotomicExtension S A B
x : B
hx : x ∈ {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1}
⊢ x ∈ {b | ∃ n_1, n_1 ∈ S ∪ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
simp only [union_singleton, mem_insert_iff, mem_setOf_eq] at hx ⊢
[GOAL]
case refine'_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ (s : ℕ+), s ∈ S → n ∣ s
hS : Set.Nonempty S
H : IsCyclotomicExtension S A B
x : B
hx : ∃ n, n ∈ S ∧ x ^ ↑n = 1
⊢ ∃ n_1, (n_1 = n ∨ n_1 ∈ S) ∧ x ^ ↑n_1 = 1
[PROOFSTEP]
obtain ⟨m, hm⟩ := hx
[GOAL]
case refine'_2.intro
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ (s : ℕ+), s ∈ S → n ∣ s
hS : Set.Nonempty S
H : IsCyclotomicExtension S A B
x : B
m : ℕ+
hm : m ∈ S ∧ x ^ ↑m = 1
⊢ ∃ n_1, (n_1 = n ∨ n_1 ∈ S) ∧ x ^ ↑n_1 = 1
[PROOFSTEP]
exact ⟨m, ⟨Or.inr hm.1, hm.2⟩⟩
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ (s : ℕ+), s ∈ S → n ∣ s
hS : Set.Nonempty S
⊢ IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {n}) A B
[PROOFSTEP]
refine' ⟨fun H => of_union_of_dvd A B h hS, fun H => (iff_adjoin_eq_top _ A _).2 ⟨fun s hs => _, _⟩⟩
[GOAL]
case refine'_1
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ (s : ℕ+), s ∈ S → n ∣ s
hS : Set.Nonempty S
H : IsCyclotomicExtension (S ∪ {n}) A B
s : ℕ+
hs : s ∈ S
⊢ ∃ r, IsPrimitiveRoot r ↑s
[PROOFSTEP]
exact H.exists_prim_root (subset_union_left _ _ hs)
[GOAL]
case refine'_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ (s : ℕ+), s ∈ S → n ∣ s
hS : Set.Nonempty S
H : IsCyclotomicExtension (S ∪ {n}) A B
⊢ adjoin A {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} = ⊤
[PROOFSTEP]
rw [_root_.eq_top_iff, ← ((iff_adjoin_eq_top _ A B).1 H).2]
[GOAL]
case refine'_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ (s : ℕ+), s ∈ S → n ∣ s
hS : Set.Nonempty S
H : IsCyclotomicExtension (S ∪ {n}) A B
⊢ adjoin A {b | ∃ n_1, n_1 ∈ S ∪ {n} ∧ b ^ ↑n_1 = 1} ≤ adjoin A {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1}
[PROOFSTEP]
refine' adjoin_mono fun x hx => _
[GOAL]
case refine'_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ (s : ℕ+), s ∈ S → n ∣ s
hS : Set.Nonempty S
H : IsCyclotomicExtension (S ∪ {n}) A B
x : B
hx : x ∈ {b | ∃ n_1, n_1 ∈ S ∪ {n} ∧ b ^ ↑n_1 = 1}
⊢ x ∈ {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1}
[PROOFSTEP]
simp only [union_singleton, mem_insert_iff, mem_setOf_eq] at hx ⊢
[GOAL]
case refine'_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ (s : ℕ+), s ∈ S → n ∣ s
hS : Set.Nonempty S
H : IsCyclotomicExtension (S ∪ {n}) A B
x : B
hx : ∃ n_1, (n_1 = n ∨ n_1 ∈ S) ∧ x ^ ↑n_1 = 1
⊢ ∃ n, n ∈ S ∧ x ^ ↑n = 1
[PROOFSTEP]
obtain ⟨m, rfl | hm, hxpow⟩ := hx
[GOAL]
case refine'_2.intro.intro.inl
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hS : Set.Nonempty S
x : B
m : ℕ+
hxpow : x ^ ↑m = 1
h : ∀ (s : ℕ+), s ∈ S → m ∣ s
H : IsCyclotomicExtension (S ∪ {m}) A B
⊢ ∃ n, n ∈ S ∧ x ^ ↑n = 1
[PROOFSTEP]
obtain ⟨y, hy⟩ := hS
[GOAL]
case refine'_2.intro.intro.inl.intro
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : B
m : ℕ+
hxpow : x ^ ↑m = 1
h : ∀ (s : ℕ+), s ∈ S → m ∣ s
H : IsCyclotomicExtension (S ∪ {m}) A B
y : ℕ+
hy : y ∈ S
⊢ ∃ n, n ∈ S ∧ x ^ ↑n = 1
[PROOFSTEP]
refine' ⟨y, ⟨hy, _⟩⟩
[GOAL]
case refine'_2.intro.intro.inl.intro
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : B
m : ℕ+
hxpow : x ^ ↑m = 1
h : ∀ (s : ℕ+), s ∈ S → m ∣ s
H : IsCyclotomicExtension (S ∪ {m}) A B
y : ℕ+
hy : y ∈ S
⊢ x ^ ↑y = 1
[PROOFSTEP]
obtain ⟨z, rfl⟩ := h y hy
[GOAL]
case refine'_2.intro.intro.inl.intro.intro
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : B
m : ℕ+
hxpow : x ^ ↑m = 1
h : ∀ (s : ℕ+), s ∈ S → m ∣ s
H : IsCyclotomicExtension (S ∪ {m}) A B
z : ℕ+
hy : m * z ∈ S
⊢ x ^ ↑(m * z) = 1
[PROOFSTEP]
simp only [PNat.mul_coe, pow_mul, hxpow, one_pow]
[GOAL]
case refine'_2.intro.intro.inr
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ∀ (s : ℕ+), s ∈ S → n ∣ s
hS : Set.Nonempty S
H : IsCyclotomicExtension (S ∪ {n}) A B
x : B
m : ℕ+
hxpow : x ^ ↑m = 1
hm : m ∈ S
⊢ ∃ n, n ∈ S ∧ x ^ ↑n = 1
[PROOFSTEP]
exact ⟨m, ⟨hm, hxpow⟩⟩
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {1}) A B
[PROOFSTEP]
obtain hS | rfl := S.eq_empty_or_nonempty.symm
[GOAL]
case inl
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hS : Set.Nonempty S
⊢ IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {1}) A B
[PROOFSTEP]
exact iff_union_of_dvd _ _ (fun s _ => one_dvd _) hS
[GOAL]
case inr
n : ℕ+
T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ IsCyclotomicExtension ∅ A B ↔ IsCyclotomicExtension (∅ ∪ {1}) A B
[PROOFSTEP]
rw [empty_union]
[GOAL]
case inr
n : ℕ+
T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ IsCyclotomicExtension ∅ A B ↔ IsCyclotomicExtension {1} A B
[PROOFSTEP]
refine' ⟨fun H => _, fun H => _⟩
[GOAL]
case inr.refine'_1
n : ℕ+
T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension ∅ A B
⊢ IsCyclotomicExtension {1} A B
[PROOFSTEP]
refine' (iff_adjoin_eq_top _ A _).2 ⟨fun s hs => ⟨1, by simp [mem_singleton_iff.1 hs]⟩, _⟩
[GOAL]
n : ℕ+
T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension ∅ A B
s : ℕ+
hs : s ∈ {1}
⊢ IsPrimitiveRoot 1 ↑s
[PROOFSTEP]
simp [mem_singleton_iff.1 hs]
[GOAL]
case inr.refine'_1
n : ℕ+
T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension ∅ A B
⊢ adjoin A {b | ∃ n, n ∈ {1} ∧ b ^ ↑n = 1} = ⊤
[PROOFSTEP]
simp [adjoin_singleton_one, empty]
[GOAL]
case inr.refine'_2
n : ℕ+
T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension {1} A B
⊢ IsCyclotomicExtension ∅ A B
[PROOFSTEP]
refine' (iff_adjoin_eq_top _ A _).2 ⟨fun s hs => (not_mem_empty s hs).elim, _⟩
[GOAL]
case inr.refine'_2
n : ℕ+
T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension {1} A B
⊢ adjoin A {b | ∃ n, n ∈ ∅ ∧ b ^ ↑n = 1} = ⊤
[PROOFSTEP]
simp [@singleton_one A B _ _ _ H]
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ⊥ = ⊤
⊢ IsCyclotomicExtension {1} A B
[PROOFSTEP]
convert (iff_union_singleton_one _ A _).1 (singleton_zero_of_bot_eq_top h)
[GOAL]
case h.e'_1
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h : ⊥ = ⊤
⊢ {1} = ∅ ∪ {1}
[PROOFSTEP]
simp
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
C : Type u_1
inst✝¹ : CommRing C
inst✝ : Algebra A C
h : IsCyclotomicExtension S A B
f : B ≃ₐ[A] C
⊢ IsCyclotomicExtension S A C
[PROOFSTEP]
letI : Algebra B C := f.toAlgHom.toRingHom.toAlgebra
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
C : Type u_1
inst✝¹ : CommRing C
inst✝ : Algebra A C
h : IsCyclotomicExtension S A B
f : B ≃ₐ[A] C
this : Algebra B C := RingHom.toAlgebra ↑↑f
⊢ IsCyclotomicExtension S A C
[PROOFSTEP]
haveI : IsCyclotomicExtension {1} B C := singleton_one_of_algebraMap_bijective f.surjective
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
C : Type u_1
inst✝¹ : CommRing C
inst✝ : Algebra A C
h : IsCyclotomicExtension S A B
f : B ≃ₐ[A] C
this✝ : Algebra B C := RingHom.toAlgebra ↑↑f
this : IsCyclotomicExtension {1} B C
⊢ IsCyclotomicExtension S A C
[PROOFSTEP]
haveI : IsScalarTower A B C := IsScalarTower.of_ring_hom f.toAlgHom
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
C : Type u_1
inst✝¹ : CommRing C
inst✝ : Algebra A C
h : IsCyclotomicExtension S A B
f : B ≃ₐ[A] C
this✝¹ : Algebra B C := RingHom.toAlgebra ↑↑f
this✝ : IsCyclotomicExtension {1} B C
this : IsScalarTower A B C
⊢ IsCyclotomicExtension S A C
[PROOFSTEP]
exact (iff_union_singleton_one _ _ _).2 (trans S {1} A B C f.injective)
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
h : IsCyclotomicExtension {n} A B
inst✝ : IsDomain B
⊢ NeZero ↑↑n
[PROOFSTEP]
obtain ⟨⟨r, hr⟩, -⟩ := (iff_singleton n A B).1 h
[GOAL]
case intro.intro
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
h : IsCyclotomicExtension {n} A B
inst✝ : IsDomain B
r : B
hr : IsPrimitiveRoot r ↑n
⊢ NeZero ↑↑n
[PROOFSTEP]
exact hr.neZero'
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsCyclotomicExtension {n} A B
inst✝ : IsDomain B
⊢ NeZero ↑↑n
[PROOFSTEP]
haveI := IsCyclotomicExtension.neZero n A B
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsCyclotomicExtension {n} A B
inst✝ : IsDomain B
this : NeZero ↑↑n
⊢ NeZero ↑↑n
[PROOFSTEP]
exact NeZero.nat_of_neZero (algebraMap A B)
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
⊢ Module.Finite A B
[PROOFSTEP]
classical
rw [Module.finite_def, ← top_toSubmodule, ← ((iff_adjoin_eq_top _ _ _).1 h).2]
refine' FG_adjoin_of_finite _ fun b hb => _
· simp only [mem_singleton_iff, exists_eq_left]
  have : {b : B | b ^ (n : ℕ) = 1} = (nthRoots n (1 : B)).toFinset :=
    Set.ext fun x => ⟨fun h => by simpa using h, fun h => by simpa using h⟩
  rw [this]
  exact (nthRoots (↑n) 1).toFinset.finite_toSet
· simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq] at hb 
  refine' ⟨X ^ (n : ℕ) - 1, ⟨monic_X_pow_sub_C _ n.pos.ne.symm, by simp [hb]⟩⟩
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
⊢ Module.Finite A B
[PROOFSTEP]
rw [Module.finite_def, ← top_toSubmodule, ← ((iff_adjoin_eq_top _ _ _).1 h).2]
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
⊢ Submodule.FG (↑Subalgebra.toSubmodule (adjoin A {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}))
[PROOFSTEP]
refine' FG_adjoin_of_finite _ fun b hb => _
[GOAL]
case refine'_1
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
⊢ Set.Finite {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
simp only [mem_singleton_iff, exists_eq_left]
[GOAL]
case refine'_1
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
⊢ Set.Finite {b | b ^ ↑n = 1}
[PROOFSTEP]
have : {b : B | b ^ (n : ℕ) = 1} = (nthRoots n (1 : B)).toFinset :=
  Set.ext fun x => ⟨fun h => by simpa using h, fun h => by simpa using h⟩
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
h✝ : IsCyclotomicExtension {n} A B
x : B
h : x ∈ {b | b ^ ↑n = 1}
⊢ x ∈ ↑(Multiset.toFinset (nthRoots (↑n) 1))
[PROOFSTEP]
simpa using h
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
h✝ : IsCyclotomicExtension {n} A B
x : B
h : x ∈ ↑(Multiset.toFinset (nthRoots (↑n) 1))
⊢ x ∈ {b | b ^ ↑n = 1}
[PROOFSTEP]
simpa using h
[GOAL]
case refine'_1
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
this : {b | b ^ ↑n = 1} = ↑(Multiset.toFinset (nthRoots (↑n) 1))
⊢ Set.Finite {b | b ^ ↑n = 1}
[PROOFSTEP]
rw [this]
[GOAL]
case refine'_1
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
this : {b | b ^ ↑n = 1} = ↑(Multiset.toFinset (nthRoots (↑n) 1))
⊢ Set.Finite ↑(Multiset.toFinset (nthRoots (↑n) 1))
[PROOFSTEP]
exact (nthRoots (↑n) 1).toFinset.finite_toSet
[GOAL]
case refine'_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
b : B
hb : b ∈ {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
⊢ IsIntegral A b
[PROOFSTEP]
simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq] at hb 
[GOAL]
case refine'_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
b : B
hb : b ^ ↑n = 1
⊢ IsIntegral A b
[PROOFSTEP]
refine' ⟨X ^ (n : ℕ) - 1, ⟨monic_X_pow_sub_C _ n.pos.ne.symm, by simp [hb]⟩⟩
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
b : B
hb : b ^ ↑n = 1
⊢ eval₂ (algebraMap A B) b (X ^ ↑n - 1) = 0
[PROOFSTEP]
simp [hb]
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
h₁ : Finite ↑S
h₂ : IsCyclotomicExtension S A B
⊢ Module.Finite A B
[PROOFSTEP]
cases' nonempty_fintype S with h
[GOAL]
case intro
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
h₁ : Finite ↑S
h₂ : IsCyclotomicExtension S A B
h : Fintype ↑S
⊢ Module.Finite A B
[PROOFSTEP]
revert h₂ A B
[GOAL]
case intro
n : ℕ+
S T : Set ℕ+
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h₁ : Finite ↑S
h : Fintype ↑S
⊢ ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
[PROOFSTEP]
refine' Set.Finite.induction_on (Set.Finite.intro h) (fun A B => _) @fun n S _ _ H A B => _
[GOAL]
case intro.refine'_1
n : ℕ+
S T : Set ℕ+
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h₁ : Finite ↑S
h : Fintype ↑S
A : Type u
B : Type v
⊢ ∀ [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
    [h₂ : IsCyclotomicExtension ∅ A B], Module.Finite A B
[PROOFSTEP]
intro _ _ _ _ _
[GOAL]
case intro.refine'_1
n : ℕ+
S T : Set ℕ+
K : Type w
L : Type z
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
h₁ : Finite ↑S
h : Fintype ↑S
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂✝ : IsCyclotomicExtension ∅ A B
⊢ Module.Finite A B
[PROOFSTEP]
refine' Module.finite_def.2 ⟨({1} : Finset B), _⟩
[GOAL]
case intro.refine'_1
n : ℕ+
S T : Set ℕ+
K : Type w
L : Type z
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
h₁ : Finite ↑S
h : Fintype ↑S
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂✝ : IsCyclotomicExtension ∅ A B
⊢ Submodule.span A ↑{1} = ⊤
[PROOFSTEP]
simp [← top_toSubmodule, ← empty, toSubmodule_bot]
[GOAL]
case intro.refine'_2
n✝ : ℕ+
S✝ T : Set ℕ+
K : Type w
L : Type z
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
h₁ : Finite ↑S✝
h : Fintype ↑S✝
n : ℕ+
S : Set ℕ+
x✝¹ : ¬n ∈ S
x✝ : Set.Finite S
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
⊢ ∀ [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
    [h₂ : IsCyclotomicExtension (insert n S) A B], Module.Finite A B
[PROOFSTEP]
intro _ _ _ _ h
[GOAL]
case intro.refine'_2
n✝ : ℕ+
S✝ T : Set ℕ+
K : Type w
L : Type z
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
h₁ : Finite ↑S✝
h✝ : Fintype ↑S✝
n : ℕ+
S : Set ℕ+
x✝¹ : ¬n ∈ S
x✝ : Set.Finite S
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension (insert n S) A B
⊢ Module.Finite A B
[PROOFSTEP]
haveI : IsCyclotomicExtension S A (adjoin A {b : B | ∃ n : ℕ+, n ∈ S ∧ b ^ (n : ℕ) = 1}) :=
  union_left _ (insert n S) _ _ (subset_insert n S)
[GOAL]
case intro.refine'_2
n✝ : ℕ+
S✝ T : Set ℕ+
K : Type w
L : Type z
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
h₁ : Finite ↑S✝
h✝ : Fintype ↑S✝
n : ℕ+
S : Set ℕ+
x✝¹ : ¬n ∈ S
x✝ : Set.Finite S
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension (insert n S) A B
this : IsCyclotomicExtension S A { x // x ∈ adjoin A {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} }
⊢ Module.Finite A B
[PROOFSTEP]
haveI := H A (adjoin A {b : B | ∃ n : ℕ+, n ∈ S ∧ b ^ (n : ℕ) = 1})
[GOAL]
case intro.refine'_2
n✝ : ℕ+
S✝ T : Set ℕ+
K : Type w
L : Type z
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
h₁ : Finite ↑S✝
h✝ : Fintype ↑S✝
n : ℕ+
S : Set ℕ+
x✝¹ : ¬n ∈ S
x✝ : Set.Finite S
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension (insert n S) A B
this✝ : IsCyclotomicExtension S A { x // x ∈ adjoin A {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} }
this : Module.Finite A { x // x ∈ adjoin A {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} }
⊢ Module.Finite A B
[PROOFSTEP]
have : Module.Finite (adjoin A {b : B | ∃ n : ℕ+, n ∈ S ∧ b ^ (n : ℕ) = 1}) B :=
  by
  rw [← union_singleton] at h 
  letI := @union_right S { n } A B _ _ _ h
  exact finite_of_singleton n _ _
[GOAL]
n✝ : ℕ+
S✝ T : Set ℕ+
K : Type w
L : Type z
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
h₁ : Finite ↑S✝
h✝ : Fintype ↑S✝
n : ℕ+
S : Set ℕ+
x✝¹ : ¬n ∈ S
x✝ : Set.Finite S
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension (insert n S) A B
this✝ : IsCyclotomicExtension S A { x // x ∈ adjoin A {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} }
this : Module.Finite A { x // x ∈ adjoin A {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} }
⊢ Module.Finite { x // x ∈ adjoin A {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} } B
[PROOFSTEP]
rw [← union_singleton] at h 
[GOAL]
n✝ : ℕ+
S✝ T : Set ℕ+
K : Type w
L : Type z
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
h₁ : Finite ↑S✝
h✝ : Fintype ↑S✝
n : ℕ+
S : Set ℕ+
x✝¹ : ¬n ∈ S
x✝ : Set.Finite S
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension (S ∪ {n}) A B
this✝ : IsCyclotomicExtension S A { x // x ∈ adjoin A {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} }
this : Module.Finite A { x // x ∈ adjoin A {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} }
⊢ Module.Finite { x // x ∈ adjoin A {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} } B
[PROOFSTEP]
letI := @union_right S { n } A B _ _ _ h
[GOAL]
n✝ : ℕ+
S✝ T : Set ℕ+
K : Type w
L : Type z
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
h₁ : Finite ↑S✝
h✝ : Fintype ↑S✝
n : ℕ+
S : Set ℕ+
x✝¹ : ¬n ∈ S
x✝ : Set.Finite S
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension (S ∪ {n}) A B
this✝¹ : IsCyclotomicExtension S A { x // x ∈ adjoin A {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} }
this✝ : Module.Finite A { x // x ∈ adjoin A {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} }
this : IsCyclotomicExtension {n} { x // x ∈ adjoin A {b | ∃ a, a ∈ S ∧ b ^ ↑a = 1} } B := union_right S {n} A B
⊢ Module.Finite { x // x ∈ adjoin A {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} } B
[PROOFSTEP]
exact finite_of_singleton n _ _
[GOAL]
case intro.refine'_2
n✝ : ℕ+
S✝ T : Set ℕ+
K : Type w
L : Type z
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
h₁ : Finite ↑S✝
h✝ : Fintype ↑S✝
n : ℕ+
S : Set ℕ+
x✝¹ : ¬n ∈ S
x✝ : Set.Finite S
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension (insert n S) A B
this✝¹ : IsCyclotomicExtension S A { x // x ∈ adjoin A {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} }
this✝ : Module.Finite A { x // x ∈ adjoin A {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} }
this : Module.Finite { x // x ∈ adjoin A {b | ∃ n, n ∈ S ∧ b ^ ↑n = 1} } B
⊢ Module.Finite A B
[PROOFSTEP]
exact Module.Finite.trans (adjoin A {b : B | ∃ n : ℕ+, n ∈ S ∧ b ^ (n : ℕ) = 1}) _
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
h : NumberField K
inst✝¹ : Finite ↑S
inst✝ : IsCyclotomicExtension S K L
⊢ FiniteDimensional ℚ L
[PROOFSTEP]
haveI := charZero_of_injective_algebraMap (algebraMap K L).injective
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
h : NumberField K
inst✝¹ : Finite ↑S
inst✝ : IsCyclotomicExtension S K L
this : CharZero L
⊢ FiniteDimensional ℚ L
[PROOFSTEP]
haveI := IsCyclotomicExtension.finite S K L
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
h : NumberField K
inst✝¹ : Finite ↑S
inst✝ : IsCyclotomicExtension S K L
this✝ : CharZero L
this : Module.Finite K L
⊢ FiniteDimensional ℚ L
[PROOFSTEP]
exact Module.Finite.trans K _
[GOAL]
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
⊢ adjoin A (rootSet (cyclotomic (↑n) A) B) = adjoin A {b | ∃ a, a ∈ {n} ∧ b ^ ↑a = 1}
[PROOFSTEP]
simp only [mem_singleton_iff, exists_eq_left, map_cyclotomic]
[GOAL]
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
⊢ adjoin A (rootSet (cyclotomic (↑n) A) B) = adjoin A {b | b ^ ↑n = 1}
[PROOFSTEP]
refine' le_antisymm (adjoin_mono fun x hx => _) (adjoin_le fun x hx => _)
[GOAL]
case refine'_1
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x ∈ rootSet (cyclotomic (↑n) A) B
⊢ x ∈ {b | b ^ ↑n = 1}
[PROOFSTEP]
rw [mem_rootSet'] at hx 
[GOAL]
case refine'_1
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : map (algebraMap A B) (cyclotomic (↑n) A) ≠ 0 ∧ ↑(aeval x) (cyclotomic (↑n) A) = 0
⊢ x ∈ {b | b ^ ↑n = 1}
[PROOFSTEP]
simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq]
[GOAL]
case refine'_1
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : map (algebraMap A B) (cyclotomic (↑n) A) ≠ 0 ∧ ↑(aeval x) (cyclotomic (↑n) A) = 0
⊢ x ^ ↑n = 1
[PROOFSTEP]
rw [isRoot_of_unity_iff n.pos]
[GOAL]
case refine'_1
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : map (algebraMap A B) (cyclotomic (↑n) A) ≠ 0 ∧ ↑(aeval x) (cyclotomic (↑n) A) = 0
⊢ ∃ i, i ∈ Nat.divisors ↑n ∧ IsRoot (cyclotomic i B) x
[PROOFSTEP]
refine' ⟨n, Nat.mem_divisors_self n n.ne_zero, _⟩
[GOAL]
case refine'_1
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : map (algebraMap A B) (cyclotomic (↑n) A) ≠ 0 ∧ ↑(aeval x) (cyclotomic (↑n) A) = 0
⊢ IsRoot (cyclotomic (↑n) B) x
[PROOFSTEP]
rw [IsRoot.def, ← map_cyclotomic n (algebraMap A B), eval_map, ← aeval_def]
[GOAL]
case refine'_1
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : map (algebraMap A B) (cyclotomic (↑n) A) ≠ 0 ∧ ↑(aeval x) (cyclotomic (↑n) A) = 0
⊢ ↑(aeval x) (cyclotomic (↑n) A) = 0
[PROOFSTEP]
exact hx.2
[GOAL]
case refine'_2
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x ∈ {b | b ^ ↑n = 1}
⊢ x ∈ ↑(adjoin A (rootSet (cyclotomic (↑n) A) B))
[PROOFSTEP]
simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq] at hx 
[GOAL]
case refine'_2
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x ^ ↑n = 1
⊢ x ∈ ↑(adjoin A (rootSet (cyclotomic (↑n) A) B))
[PROOFSTEP]
obtain ⟨i, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx n.pos
[GOAL]
case refine'_2.intro.intro
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
i : ℕ
left✝ : i < ↑n
hx : (ζ ^ i) ^ ↑n = 1
⊢ ζ ^ i ∈ ↑(adjoin A (rootSet (cyclotomic (↑n) A) B))
[PROOFSTEP]
refine' SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin _) _)
[GOAL]
case refine'_2.intro.intro
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
i : ℕ
left✝ : i < ↑n
hx : (ζ ^ i) ^ ↑n = 1
⊢ ζ ∈ rootSet (cyclotomic (↑n) A) B
[PROOFSTEP]
rw [mem_rootSet', map_cyclotomic, aeval_def, ← eval_map, map_cyclotomic, ← IsRoot]
[GOAL]
case refine'_2.intro.intro
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
i : ℕ
left✝ : i < ↑n
hx : (ζ ^ i) ^ ↑n = 1
⊢ cyclotomic (↑n) B ≠ 0 ∧ IsRoot (cyclotomic (↑n) B) ζ
[PROOFSTEP]
refine' ⟨cyclotomic_ne_zero n B, hζ.isRoot_cyclotomic n.pos⟩
[GOAL]
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
n : ℕ+
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
⊢ adjoin A (rootSet (cyclotomic (↑n) A) B) = adjoin A {ζ}
[PROOFSTEP]
refine' le_antisymm (adjoin_le fun x hx => _) (adjoin_mono fun x hx => _)
[GOAL]
case refine'_1
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
n : ℕ+
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x ∈ rootSet (cyclotomic (↑n) A) B
⊢ x ∈ ↑(adjoin A {ζ})
[PROOFSTEP]
suffices hx : x ^ n.1 = 1
[GOAL]
case refine'_1
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
n : ℕ+
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx✝ : x ∈ rootSet (cyclotomic (↑n) A) B
hx : x ^ ↑n = 1
⊢ x ∈ ↑(adjoin A {ζ})
case hx
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
n : ℕ+
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x ∈ rootSet (cyclotomic (↑n) A) B
⊢ x ^ ↑n = 1
[PROOFSTEP]
obtain ⟨i, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx n.pos
[GOAL]
case refine'_1.intro.intro
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
n : ℕ+
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
i : ℕ
left✝ : i < ↑n
hx✝ : ζ ^ i ∈ rootSet (cyclotomic (↑n) A) B
hx : (ζ ^ i) ^ ↑n = 1
⊢ ζ ^ i ∈ ↑(adjoin A {ζ})
case hx
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
n : ℕ+
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x ∈ rootSet (cyclotomic (↑n) A) B
⊢ x ^ ↑n = 1
[PROOFSTEP]
exact SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin <| mem_singleton ζ) _)
[GOAL]
case hx
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
n : ℕ+
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x ∈ rootSet (cyclotomic (↑n) A) B
⊢ x ^ ↑n = 1
[PROOFSTEP]
refine' (isRoot_of_unity_iff n.pos B).2 _
[GOAL]
case hx
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
n : ℕ+
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x ∈ rootSet (cyclotomic (↑n) A) B
⊢ ∃ i, i ∈ Nat.divisors ↑n ∧ IsRoot (cyclotomic i B) x
[PROOFSTEP]
refine' ⟨n, Nat.mem_divisors_self n n.ne_zero, _⟩
[GOAL]
case hx
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
n : ℕ+
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x ∈ rootSet (cyclotomic (↑n) A) B
⊢ IsRoot (cyclotomic (↑n) B) x
[PROOFSTEP]
rw [mem_rootSet', aeval_def, ← eval_map, map_cyclotomic, ← IsRoot] at hx 
[GOAL]
case hx
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
n : ℕ+
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : cyclotomic (↑n) B ≠ 0 ∧ IsRoot (cyclotomic (↑n) B) x
⊢ IsRoot (cyclotomic (↑n) B) x
[PROOFSTEP]
exact hx.2
[GOAL]
case refine'_2
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
n : ℕ+
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x ∈ {ζ}
⊢ x ∈ rootSet (cyclotomic (↑n) A) B
[PROOFSTEP]
simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq] at hx 
[GOAL]
case refine'_2
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
n : ℕ+
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x = ζ
⊢ x ∈ rootSet (cyclotomic (↑n) A) B
[PROOFSTEP]
simpa only [hx, mem_rootSet', map_cyclotomic, aeval_def, ← eval_map, IsRoot] using
  And.intro (cyclotomic_ne_zero n B) (hζ.isRoot_cyclotomic n.pos)
[GOAL]
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
n : ℕ+
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
⊢ adjoin A {ζ} = ⊤
[PROOFSTEP]
classical
rw [← adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic hζ]
rw [adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ]
exact ((iff_adjoin_eq_top { n } A B).mp h).2
[GOAL]
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
n : ℕ+
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
⊢ adjoin A {ζ} = ⊤
[PROOFSTEP]
rw [← adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic hζ]
[GOAL]
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
n : ℕ+
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
⊢ adjoin A (rootSet (cyclotomic (↑n) A) B) = ⊤
[PROOFSTEP]
rw [adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ]
[GOAL]
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
n : ℕ+
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
⊢ adjoin A {b | ∃ a, a ∈ {n} ∧ b ^ ↑a = 1} = ⊤
[PROOFSTEP]
exact ((iff_adjoin_eq_top { n } A B).mp h).2
[GOAL]
n✝¹ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
n✝ : ℕ+
hi : n✝ ∈ {n}
⊢ ∃ r, IsPrimitiveRoot r ↑n✝
[PROOFSTEP]
rw [Set.mem_singleton_iff] at hi 
[GOAL]
n✝¹ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
n✝ : ℕ+
hi : n✝ = n
⊢ ∃ r, IsPrimitiveRoot r ↑n✝
[PROOFSTEP]
refine' ⟨⟨ζ, subset_adjoin <| Set.mem_singleton ζ⟩, _⟩
[GOAL]
n✝¹ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
n✝ : ℕ+
hi : n✝ = n
⊢ IsPrimitiveRoot { val := ζ, property := (_ : ζ ∈ ↑(adjoin A {ζ})) } ↑n✝
[PROOFSTEP]
rwa [← IsPrimitiveRoot.coe_submonoidClass_iff, Subtype.coe_mk, hi]
[GOAL]
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x : { x // x ∈ adjoin A {ζ} }
⊢ x ∈ adjoin A {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
refine adjoin_induction' (x := x) (fun b hb => ?_) (fun a => ?_) (fun b₁ b₂ hb₁ hb₂ => ?_) (fun b₁ b₂ hb₁ hb₂ => ?_)
[GOAL]
case refine_1
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x : { x // x ∈ adjoin A {ζ} }
b : B
hb : b ∈ {ζ}
⊢ { val := b, property := (_ : b ∈ ↑(adjoin A {ζ})) } ∈ adjoin A {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
rw [Set.mem_singleton_iff] at hb 
[GOAL]
case refine_1
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x : { x // x ∈ adjoin A {ζ} }
b : B
hb✝ : b ∈ {ζ}
hb : b = ζ
⊢ { val := b, property := (_ : b ∈ ↑(adjoin A {ζ})) } ∈ adjoin A {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
refine' subset_adjoin _
[GOAL]
case refine_1
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x : { x // x ∈ adjoin A {ζ} }
b : B
hb✝ : b ∈ {ζ}
hb : b = ζ
⊢ { val := b, property := (_ : b ∈ ↑(adjoin A {ζ})) } ∈ {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq, hb]
[GOAL]
case refine_1
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x : { x // x ∈ adjoin A {ζ} }
b : B
hb✝ : b ∈ {ζ}
hb : b = ζ
⊢ { val := ζ, property := (_ : (fun x => x ∈ adjoin A {ζ}) ζ) } ^ ↑n = 1
[PROOFSTEP]
rw [← Subalgebra.coe_eq_one, Subalgebra.coe_pow, Subtype.coe_mk]
[GOAL]
case refine_1
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x : { x // x ∈ adjoin A {ζ} }
b : B
hb✝ : b ∈ {ζ}
hb : b = ζ
⊢ ζ ^ ↑n = 1
[PROOFSTEP]
exact ((IsPrimitiveRoot.iff_def ζ n).1 h).1
[GOAL]
case refine_2
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x : { x // x ∈ adjoin A {ζ} }
a : A
⊢ ↑(algebraMap A { x // x ∈ adjoin A {ζ} }) a ∈ adjoin A {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
exact Subalgebra.algebraMap_mem _ _
[GOAL]
case refine_3
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x b₁ b₂ : { x // x ∈ adjoin A {ζ} }
hb₁ : b₁ ∈ adjoin A {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
hb₂ : b₂ ∈ adjoin A {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
⊢ b₁ + b₂ ∈ adjoin A {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
exact Subalgebra.add_mem _ hb₁ hb₂
[GOAL]
case refine_4
n✝ : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x b₁ b₂ : { x // x ∈ adjoin A {ζ} }
hb₁ : b₁ ∈ adjoin A {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
hb₂ : b₂ ∈ adjoin A {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
⊢ b₁ * b₂ ∈ adjoin A {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
exact Subalgebra.mul_mem _ hb₁ hb₂
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ Splits (algebraMap K L) (X ^ ↑n - 1)
[PROOFSTEP]
rw [← splits_id_iff_splits, Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow, Polynomial.map_X]
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ Splits (RingHom.id L) (X ^ ↑n - 1)
[PROOFSTEP]
obtain ⟨z, hz⟩ := ((IsCyclotomicExtension_iff _ _ _).1 H).1 hS
[GOAL]
case intro
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : IsCyclotomicExtension S K L
hS : n ∈ S
z : L
hz : IsPrimitiveRoot z ↑n
⊢ Splits (RingHom.id L) (X ^ ↑n - 1)
[PROOFSTEP]
exact X_pow_sub_one_splits hz
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ Splits (algebraMap K L) (cyclotomic (↑n) K)
[PROOFSTEP]
refine' splits_of_splits_of_dvd _ (X_pow_sub_C_ne_zero n.pos _) (splits_X_pow_sub_one K L hS) _
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ cyclotomic (↑n) K ∣ X ^ ↑n - ↑C 1
[PROOFSTEP]
use∏ i : ℕ in (n : ℕ).properDivisors, Polynomial.cyclotomic i K
[GOAL]
case h
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ X ^ ↑n - ↑C 1 = cyclotomic (↑n) K * ∏ i in Nat.properDivisors ↑n, cyclotomic i K
[PROOFSTEP]
rw [(eq_cyclotomic_iff n.pos _).1 rfl, RingHom.map_one]
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
⊢ adjoin K (rootSet (X ^ ↑n - 1) L) = ⊤
[PROOFSTEP]
rw [← ((iff_adjoin_eq_top { n } K L).1 inferInstance).2]
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
⊢ adjoin K (rootSet (X ^ ↑n - 1) L) = adjoin K {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
congr
[GOAL]
case e_s
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
⊢ rootSet (X ^ ↑n - 1) L = {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
refine' Set.ext fun x => _
[GOAL]
case e_s
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
x : L
⊢ x ∈ rootSet (X ^ ↑n - 1) L ↔ x ∈ {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
simp only [Polynomial.map_pow, mem_singleton_iff, Multiset.mem_toFinset, exists_eq_left, mem_setOf_eq, Polynomial.map_X,
  Polynomial.map_one, Finset.mem_coe, Polynomial.map_sub]
[GOAL]
case e_s
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
x : L
⊢ x ∈ rootSet (X ^ ↑n - 1) L ↔ x ^ ↑n = 1
[PROOFSTEP]
simp only [mem_rootSet', map_sub, map_pow, aeval_one, aeval_X, sub_eq_zero, map_X, and_iff_right_iff_imp,
  Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_one]
[GOAL]
case e_s
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
x : L
⊢ x ^ ↑n = 1 → X ^ ↑n - 1 ≠ 0
[PROOFSTEP]
exact fun _ => X_pow_sub_C_ne_zero n.pos (1 : L)
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
⊢ adjoin K (rootSet (cyclotomic (↑n) K) L) = ⊤
[PROOFSTEP]
rw [← ((iff_adjoin_eq_top { n } K L).1 inferInstance).2]
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
⊢ adjoin K (rootSet (cyclotomic (↑n) K) L) = adjoin K {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
letI := Classical.decEq L
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
this : DecidableEq L := Classical.decEq L
⊢ adjoin K (rootSet (cyclotomic (↑n) K) L) = adjoin K {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
obtain ⟨ζ : L, hζ⟩ := IsCyclotomicExtension.exists_prim_root K (B := L) (mem_singleton n)
[GOAL]
case intro
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
this : DecidableEq L := Classical.decEq L
ζ : L
hζ : IsPrimitiveRoot ζ ↑n
⊢ adjoin K (rootSet (cyclotomic (↑n) K) L) = adjoin K {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
exact adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Field (CyclotomicField n K)
[PROOFSTEP]
delta CyclotomicField
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Field (SplittingField (cyclotomic (↑n) K))
[PROOFSTEP]
infer_instance
  --Porting note: could not be derived
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Algebra K (CyclotomicField n K)
[PROOFSTEP]
delta CyclotomicField
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Algebra K (SplittingField (cyclotomic (↑n) K))
[PROOFSTEP]
infer_instance
  --Porting note: could not be derived
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Inhabited (CyclotomicField n K)
[PROOFSTEP]
delta CyclotomicField
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ Inhabited (SplittingField (cyclotomic (↑n) K))
[PROOFSTEP]
infer_instance
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : NeZero ↑↑n
⊢ IsCyclotomicExtension {n} K (CyclotomicField n K)
[PROOFSTEP]
haveI : NeZero ((n : ℕ) : CyclotomicField n K) := NeZero.nat_of_injective (algebraMap K _).injective
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : NeZero ↑↑n
this : NeZero ↑↑n
⊢ IsCyclotomicExtension {n} K (CyclotomicField n K)
[PROOFSTEP]
letI := Classical.decEq (CyclotomicField n K)
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : NeZero ↑↑n
this✝ : NeZero ↑↑n
this : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
⊢ IsCyclotomicExtension {n} K (CyclotomicField n K)
[PROOFSTEP]
obtain ⟨ζ, hζ⟩ :=
  exists_root_of_splits (algebraMap K (CyclotomicField n K)) (SplittingField.splits _)
    (degree_cyclotomic_pos n K n.pos).ne'
[GOAL]
case intro
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : NeZero ↑↑n
this✝ : NeZero ↑↑n
this : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
ζ : CyclotomicField n K
hζ : eval₂ (algebraMap K (CyclotomicField n K)) ζ (cyclotomic (↑n) K) = 0
⊢ IsCyclotomicExtension {n} K (CyclotomicField n K)
[PROOFSTEP]
rw [← eval_map, ← IsRoot.def, map_cyclotomic, isRoot_cyclotomic_iff] at hζ 
[GOAL]
case intro
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : NeZero ↑↑n
this✝ : NeZero ↑↑n
this : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
ζ : CyclotomicField n K
hζ : IsPrimitiveRoot ζ ↑n
⊢ IsCyclotomicExtension {n} K (CyclotomicField n K)
[PROOFSTEP]
refine ⟨?_, ?_⟩
[GOAL]
case intro.refine_1
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : NeZero ↑↑n
this✝ : NeZero ↑↑n
this : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
ζ : CyclotomicField n K
hζ : IsPrimitiveRoot ζ ↑n
⊢ ∀ {n_1 : ℕ+}, n_1 ∈ {n} → ∃ r, IsPrimitiveRoot r ↑n_1
[PROOFSTEP]
simp only [mem_singleton_iff, forall_eq]
[GOAL]
case intro.refine_1
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : NeZero ↑↑n
this✝ : NeZero ↑↑n
this : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
ζ : CyclotomicField n K
hζ : IsPrimitiveRoot ζ ↑n
⊢ ∃ r, IsPrimitiveRoot r ↑n
[PROOFSTEP]
exact ⟨ζ, hζ⟩
[GOAL]
case intro.refine_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : NeZero ↑↑n
this✝ : NeZero ↑↑n
this : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
ζ : CyclotomicField n K
hζ : IsPrimitiveRoot ζ ↑n
⊢ ∀ (x : CyclotomicField n K), x ∈ adjoin K {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
rw [← Algebra.eq_top_iff, ← SplittingField.adjoin_rootSet, eq_comm]
[GOAL]
case intro.refine_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : NeZero ↑↑n
this✝ : NeZero ↑↑n
this : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
ζ : CyclotomicField n K
hζ : IsPrimitiveRoot ζ ↑n
⊢ adjoin K (rootSet (cyclotomic (↑n) K) (SplittingField (cyclotomic (↑n) K))) =
    adjoin K {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
exact IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ NoZeroSMulDivisors A (CyclotomicField n K)
[PROOFSTEP]
refine' NoZeroSMulDivisors.of_algebraMap_injective _
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ Function.Injective ↑(algebraMap A (CyclotomicField n K))
[PROOFSTEP]
rw [IsScalarTower.algebraMap_eq A K (CyclotomicField n K)]
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ Function.Injective ↑(RingHom.comp (algebraMap K (CyclotomicField n K)) (algebraMap A K))
[PROOFSTEP]
exact
  (Function.Injective.comp (NoZeroSMulDivisors.algebraMap_injective K (CyclotomicField n K))
      (IsFractionRing.injective A K) :
    _)
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ CommRing (CyclotomicRing n A K)
[PROOFSTEP]
delta CyclotomicRing
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ CommRing { x // x ∈ adjoin A {b | b ^ ↑n = 1} }
[PROOFSTEP]
infer_instance
  --Porting note: could not be derived
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ IsDomain (CyclotomicRing n A K)
[PROOFSTEP]
delta CyclotomicRing
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ IsDomain { x // x ∈ adjoin A {b | b ^ ↑n = 1} }
[PROOFSTEP]
infer_instance
  --Porting note: could not be derived
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ Inhabited (CyclotomicRing n A K)
[PROOFSTEP]
delta CyclotomicRing
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ Inhabited { x // x ∈ adjoin A {b | b ^ ↑n = 1} }
[PROOFSTEP]
infer_instance
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑↑n
a : ℕ+
han : a ∈ {n}
⊢ ∃ r, IsPrimitiveRoot r ↑a
[PROOFSTEP]
rw [mem_singleton_iff] at han 
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑↑n
a : ℕ+
han : a = n
⊢ ∃ r, IsPrimitiveRoot r ↑a
[PROOFSTEP]
subst a
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑↑n
⊢ ∃ r, IsPrimitiveRoot r ↑n
[PROOFSTEP]
haveI := NeZero.of_noZeroSMulDivisors A K n
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑↑n
this : NeZero ↑↑n
⊢ ∃ r, IsPrimitiveRoot r ↑n
[PROOFSTEP]
haveI := NeZero.of_noZeroSMulDivisors A (CyclotomicField n K) n
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑↑n
this✝ : NeZero ↑↑n
this : NeZero ↑↑n
⊢ ∃ r, IsPrimitiveRoot r ↑n
[PROOFSTEP]
obtain ⟨μ, hμ⟩ := (CyclotomicField.isCyclotomicExtension n K).exists_prim_root (mem_singleton n)
[GOAL]
case intro
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑↑n
this✝ : NeZero ↑↑n
this : NeZero ↑↑n
μ : CyclotomicField n K
hμ : IsPrimitiveRoot μ ↑n
⊢ ∃ r, IsPrimitiveRoot r ↑n
[PROOFSTEP]
refine' ⟨⟨μ, subset_adjoin _⟩, _⟩
[GOAL]
case intro.refine'_1
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑↑n
this✝ : NeZero ↑↑n
this : NeZero ↑↑n
μ : CyclotomicField n K
hμ : IsPrimitiveRoot μ ↑n
⊢ μ ∈ {b | b ^ ↑n = 1}
[PROOFSTEP]
apply (isRoot_of_unity_iff n.pos (CyclotomicField n K)).mpr
[GOAL]
case intro.refine'_1
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑↑n
this✝ : NeZero ↑↑n
this : NeZero ↑↑n
μ : CyclotomicField n K
hμ : IsPrimitiveRoot μ ↑n
⊢ ∃ i, i ∈ Nat.divisors ↑n ∧ IsRoot (cyclotomic i (CyclotomicField n K)) μ
[PROOFSTEP]
refine' ⟨n, Nat.mem_divisors_self _ n.ne_zero, _⟩
[GOAL]
case intro.refine'_1
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑↑n
this✝ : NeZero ↑↑n
this : NeZero ↑↑n
μ : CyclotomicField n K
hμ : IsPrimitiveRoot μ ↑n
⊢ IsRoot (cyclotomic (↑n) (CyclotomicField n K)) μ
[PROOFSTEP]
rwa [← isRoot_cyclotomic_iff] at hμ 
[GOAL]
case intro.refine'_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑↑n
this✝ : NeZero ↑↑n
this : NeZero ↑↑n
μ : CyclotomicField n K
hμ : IsPrimitiveRoot μ ↑n
⊢ IsPrimitiveRoot { val := μ, property := (_ : μ ∈ ↑(adjoin A {b | b ^ ↑n = 1})) } ↑n
[PROOFSTEP]
rwa [← IsPrimitiveRoot.coe_submonoidClass_iff, Subtype.coe_mk]
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑↑n
x : CyclotomicRing n A K
⊢ x ∈ adjoin A {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
refine' adjoin_induction' (fun y hy => _) (fun a => _) (fun y z hy hz => _) (fun y z hy hz => _) x
[GOAL]
case refine'_1
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑↑n
x : CyclotomicRing n A K
y : CyclotomicField n K
hy : y ∈ {b | b ^ ↑n = 1}
⊢ { val := y, property := (_ : y ∈ ↑(adjoin A {b | b ^ ↑n = 1})) } ∈ adjoin A {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
refine' subset_adjoin _
[GOAL]
case refine'_1
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑↑n
x : CyclotomicRing n A K
y : CyclotomicField n K
hy : y ∈ {b | b ^ ↑n = 1}
⊢ { val := y, property := (_ : y ∈ ↑(adjoin A {b | b ^ ↑n = 1})) } ∈ {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq]
[GOAL]
case refine'_1
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑↑n
x : CyclotomicRing n A K
y : CyclotomicField n K
hy : y ∈ {b | b ^ ↑n = 1}
⊢ { val := y, property := (_ : y ∈ ↑(adjoin A {b | b ^ ↑n = 1})) } ^ ↑n = 1
[PROOFSTEP]
rwa [← Subalgebra.coe_eq_one, Subalgebra.coe_pow, Subtype.coe_mk]
[GOAL]
case refine'_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑↑n
x : CyclotomicRing n A K
a : A
⊢ ↑(algebraMap A { x // x ∈ adjoin A {b | b ^ ↑n = 1} }) a ∈ adjoin A {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
exact Subalgebra.algebraMap_mem _ a
[GOAL]
case refine'_3
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑↑n
x : CyclotomicRing n A K
y z : { x // x ∈ adjoin A {b | b ^ ↑n = 1} }
hy : y ∈ adjoin A {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
hz : z ∈ adjoin A {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
⊢ y + z ∈ adjoin A {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
exact Subalgebra.add_mem _ hy hz
[GOAL]
case refine'_4
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : NeZero ↑↑n
x : CyclotomicRing n A K
y z : { x // x ∈ adjoin A {b | b ^ ↑n = 1} }
hy : y ∈ adjoin A {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
hz : z ∈ adjoin A {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
⊢ y * z ∈ adjoin A {b | ∃ n_1, n_1 ∈ {n} ∧ b ^ ↑n_1 = 1}
[PROOFSTEP]
exact Subalgebra.mul_mem _ hy hz
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x✝ : { x // x ∈ nonZeroDivisors (CyclotomicRing n A K) }
x : CyclotomicRing n A K
hx : x ∈ nonZeroDivisors (CyclotomicRing n A K)
⊢ IsUnit (↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑{ val := x, property := hx })
[PROOFSTEP]
rw [isUnit_iff_ne_zero]
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x✝ : { x // x ∈ nonZeroDivisors (CyclotomicRing n A K) }
x : CyclotomicRing n A K
hx : x ∈ nonZeroDivisors (CyclotomicRing n A K)
⊢ ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑{ val := x, property := hx } ≠ 0
[PROOFSTEP]
apply map_ne_zero_of_mem_nonZeroDivisors
[GOAL]
case hg
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x✝ : { x // x ∈ nonZeroDivisors (CyclotomicRing n A K) }
x : CyclotomicRing n A K
hx : x ∈ nonZeroDivisors (CyclotomicRing n A K)
⊢ Function.Injective ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K))
case h
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x✝ : { x // x ∈ nonZeroDivisors (CyclotomicRing n A K) }
x : CyclotomicRing n A K
hx : x ∈ nonZeroDivisors (CyclotomicRing n A K)
⊢ ↑{ val := x, property := hx } ∈ nonZeroDivisors (CyclotomicRing n A K)
[PROOFSTEP]
apply adjoin_algebra_injective
[GOAL]
case h
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x✝ : { x // x ∈ nonZeroDivisors (CyclotomicRing n A K) }
x : CyclotomicRing n A K
hx : x ∈ nonZeroDivisors (CyclotomicRing n A K)
⊢ ↑{ val := x, property := hx } ∈ nonZeroDivisors (CyclotomicRing n A K)
[PROOFSTEP]
exact hx
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x : CyclotomicField n K
⊢ ∃ x_1,
    x * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x_1.snd =
      ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x_1.fst
[PROOFSTEP]
letI : NeZero ((n : ℕ) : K) := NeZero.nat_of_injective (IsFractionRing.injective A K)
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x : CyclotomicField n K
this : NeZero ↑↑n := NeZero.nat_of_injective (IsFractionRing.injective A K)
⊢ ∃ x_1,
    x * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x_1.snd =
      ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x_1.fst
[PROOFSTEP]
refine
  Algebra.adjoin_induction
    (((IsCyclotomicExtension.iff_singleton n K (CyclotomicField n K)).1 (CyclotomicField.isCyclotomicExtension n K)).2
      x)
    (fun y hy => ?_) (fun k => ?_) ?_
    ?_
      -- Porting note: the last goal was `by simpa` that now fails.
[GOAL]
case refine_1
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x : CyclotomicField n K
this : NeZero ↑↑n := NeZero.nat_of_injective (IsFractionRing.injective A K)
y : CyclotomicField n K
hy : y ∈ {b | b ^ ↑n = 1}
⊢ ∃ x,
    y * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x.snd =
      ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x.fst
[PROOFSTEP]
exact ⟨⟨⟨y, subset_adjoin hy⟩, 1⟩, by simp; rfl⟩
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x : CyclotomicField n K
this : NeZero ↑↑n := NeZero.nat_of_injective (IsFractionRing.injective A K)
y : CyclotomicField n K
hy : y ∈ {b | b ^ ↑n = 1}
⊢ y *
      ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K))
        ↑({ val := y, property := (_ : y ∈ ↑(adjoin A {b | b ^ ↑n = 1})) }, 1).snd =
    ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K))
      ({ val := y, property := (_ : y ∈ ↑(adjoin A {b | b ^ ↑n = 1})) }, 1).fst
[PROOFSTEP]
simp
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x : CyclotomicField n K
this : NeZero ↑↑n := NeZero.nat_of_injective (IsFractionRing.injective A K)
y : CyclotomicField n K
hy : y ∈ {b | b ^ ↑n = 1}
⊢ y =
    ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K))
      { val := y, property := (_ : y ∈ ↑(adjoin A {b | b ^ ↑n = 1})) }
[PROOFSTEP]
rfl
[GOAL]
case refine_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x : CyclotomicField n K
this : NeZero ↑↑n := NeZero.nat_of_injective (IsFractionRing.injective A K)
k : K
⊢ ∃ x,
    ↑(algebraMap K (CyclotomicField n K)) k * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x.snd =
      ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x.fst
[PROOFSTEP]
have : IsLocalization (nonZeroDivisors A) K := inferInstance
[GOAL]
case refine_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x : CyclotomicField n K
this✝ : NeZero ↑↑n := NeZero.nat_of_injective (IsFractionRing.injective A K)
k : K
this : IsLocalization (nonZeroDivisors A) K
⊢ ∃ x,
    ↑(algebraMap K (CyclotomicField n K)) k * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x.snd =
      ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x.fst
[PROOFSTEP]
replace := this.surj
[GOAL]
case refine_2
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x : CyclotomicField n K
this✝ : NeZero ↑↑n := NeZero.nat_of_injective (IsFractionRing.injective A K)
k : K
this : ∀ (z : K), ∃ x, z * ↑(algebraMap A K) ↑x.snd = ↑(algebraMap A K) x.fst
⊢ ∃ x,
    ↑(algebraMap K (CyclotomicField n K)) k * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x.snd =
      ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x.fst
[PROOFSTEP]
obtain ⟨⟨z, w⟩, hw⟩ := this k
[GOAL]
case refine_2.intro.mk
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x : CyclotomicField n K
this✝ : NeZero ↑↑n := NeZero.nat_of_injective (IsFractionRing.injective A K)
k : K
this : ∀ (z : K), ∃ x, z * ↑(algebraMap A K) ↑x.snd = ↑(algebraMap A K) x.fst
z : A
w : { x // x ∈ nonZeroDivisors A }
hw : k * ↑(algebraMap A K) ↑(z, w).snd = ↑(algebraMap A K) (z, w).fst
⊢ ∃ x,
    ↑(algebraMap K (CyclotomicField n K)) k * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x.snd =
      ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x.fst
[PROOFSTEP]
refine'
  ⟨⟨algebraMap A (CyclotomicRing n A K) z, algebraMap A (CyclotomicRing n A K) w,
      map_mem_nonZeroDivisors _ (algebraBase_injective n A K) w.2⟩,
    _⟩
[GOAL]
case refine_2.intro.mk
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x : CyclotomicField n K
this✝ : NeZero ↑↑n := NeZero.nat_of_injective (IsFractionRing.injective A K)
k : K
this : ∀ (z : K), ∃ x, z * ↑(algebraMap A K) ↑x.snd = ↑(algebraMap A K) x.fst
z : A
w : { x // x ∈ nonZeroDivisors A }
hw : k * ↑(algebraMap A K) ↑(z, w).snd = ↑(algebraMap A K) (z, w).fst
⊢ ↑(algebraMap K (CyclotomicField n K)) k *
      ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K))
        ↑(↑(algebraMap A (CyclotomicRing n A K)) z,
              { val := ↑(algebraMap A (CyclotomicRing n A K)) ↑w,
                property :=
                  (_ : ↑(algebraMap A (CyclotomicRing n A K)) ↑w ∈ nonZeroDivisors (CyclotomicRing n A K)) }).snd =
    ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K))
      (↑(algebraMap A (CyclotomicRing n A K)) z,
          { val := ↑(algebraMap A (CyclotomicRing n A K)) ↑w,
            property := (_ : ↑(algebraMap A (CyclotomicRing n A K)) ↑w ∈ nonZeroDivisors (CyclotomicRing n A K)) }).fst
[PROOFSTEP]
letI : IsScalarTower A K (CyclotomicField n K) := IsScalarTower.of_algebraMap_eq (congr_fun rfl)
[GOAL]
case refine_2.intro.mk
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x : CyclotomicField n K
this✝¹ : NeZero ↑↑n := NeZero.nat_of_injective (IsFractionRing.injective A K)
k : K
this✝ : ∀ (z : K), ∃ x, z * ↑(algebraMap A K) ↑x.snd = ↑(algebraMap A K) x.fst
z : A
w : { x // x ∈ nonZeroDivisors A }
hw : k * ↑(algebraMap A K) ↑(z, w).snd = ↑(algebraMap A K) (z, w).fst
this : IsScalarTower A K (CyclotomicField n K) := IsScalarTower.of_algebraMap_eq (congr_fun rfl)
⊢ ↑(algebraMap K (CyclotomicField n K)) k *
      ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K))
        ↑(↑(algebraMap A (CyclotomicRing n A K)) z,
              { val := ↑(algebraMap A (CyclotomicRing n A K)) ↑w,
                property :=
                  (_ : ↑(algebraMap A (CyclotomicRing n A K)) ↑w ∈ nonZeroDivisors (CyclotomicRing n A K)) }).snd =
    ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K))
      (↑(algebraMap A (CyclotomicRing n A K)) z,
          { val := ↑(algebraMap A (CyclotomicRing n A K)) ↑w,
            property := (_ : ↑(algebraMap A (CyclotomicRing n A K)) ↑w ∈ nonZeroDivisors (CyclotomicRing n A K)) }).fst
[PROOFSTEP]
rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
  @IsScalarTower.algebraMap_apply A K _ _ _ _ _ (_root_.CyclotomicField.algebra n K) _ _ w, ← RingHom.map_mul, hw, ←
  IsScalarTower.algebraMap_apply]
[GOAL]
case refine_3
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x : CyclotomicField n K
this : NeZero ↑↑n := NeZero.nat_of_injective (IsFractionRing.injective A K)
⊢ ∀ (x y : CyclotomicField n K),
    (∃ x_1,
        x * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x_1.snd =
          ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x_1.fst) →
      (∃ x,
          y * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x.snd =
            ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x.fst) →
        ∃ x_1,
          (x + y) * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x_1.snd =
            ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x_1.fst
[PROOFSTEP]
rintro y z ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case refine_3.intro.intro
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x : CyclotomicField n K
this : NeZero ↑↑n := NeZero.nat_of_injective (IsFractionRing.injective A K)
y z : CyclotomicField n K
a : CyclotomicRing n A K × { x // x ∈ nonZeroDivisors (CyclotomicRing n A K) }
ha :
  y * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.snd =
    ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) a.fst
b : CyclotomicRing n A K × { x // x ∈ nonZeroDivisors (CyclotomicRing n A K) }
hb :
  z * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.snd =
    ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) b.fst
⊢ ∃ x,
    (y + z) * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x.snd =
      ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x.fst
[PROOFSTEP]
refine' ⟨⟨a.1 * b.2 + b.1 * a.2, a.2 * b.2, mul_mem_nonZeroDivisors.2 ⟨a.2.2, b.2.2⟩⟩, _⟩
[GOAL]
case refine_3.intro.intro
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x : CyclotomicField n K
this : NeZero ↑↑n := NeZero.nat_of_injective (IsFractionRing.injective A K)
y z : CyclotomicField n K
a : CyclotomicRing n A K × { x // x ∈ nonZeroDivisors (CyclotomicRing n A K) }
ha :
  y * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.snd =
    ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) a.fst
b : CyclotomicRing n A K × { x // x ∈ nonZeroDivisors (CyclotomicRing n A K) }
hb :
  z * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.snd =
    ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) b.fst
⊢ (y + z) *
      ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K))
        ↑(a.fst * ↑b.snd + b.fst * ↑a.snd,
              { val := ↑a.snd * ↑b.snd,
                property := (_ : ↑a.snd * ↑b.snd ∈ nonZeroDivisors (CyclotomicRing n A K)) }).snd =
    ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K))
      (a.fst * ↑b.snd + b.fst * ↑a.snd,
          { val := ↑a.snd * ↑b.snd, property := (_ : ↑a.snd * ↑b.snd ∈ nonZeroDivisors (CyclotomicRing n A K)) }).fst
[PROOFSTEP]
rw [RingHom.map_mul, add_mul, ← mul_assoc, ha, mul_comm ((algebraMap (CyclotomicRing n A K) _) ↑a.2), ← mul_assoc, hb]
[GOAL]
case refine_3.intro.intro
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x : CyclotomicField n K
this : NeZero ↑↑n := NeZero.nat_of_injective (IsFractionRing.injective A K)
y z : CyclotomicField n K
a : CyclotomicRing n A K × { x // x ∈ nonZeroDivisors (CyclotomicRing n A K) }
ha :
  y * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.snd =
    ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) a.fst
b : CyclotomicRing n A K × { x // x ∈ nonZeroDivisors (CyclotomicRing n A K) }
hb :
  z * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.snd =
    ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) b.fst
⊢ ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) a.fst *
        ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.snd +
      ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) b.fst *
        ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.snd =
    ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K))
      (a.fst * ↑b.snd + b.fst * ↑a.snd,
          { val := ↑a.snd * ↑b.snd, property := (_ : ↑a.snd * ↑b.snd ∈ nonZeroDivisors (CyclotomicRing n A K)) }).fst
[PROOFSTEP]
simp only [map_add, map_mul]
[GOAL]
case refine_4
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x : CyclotomicField n K
this : NeZero ↑↑n := NeZero.nat_of_injective (IsFractionRing.injective A K)
⊢ ∀ (x y : CyclotomicField n K),
    (∃ x_1,
        x * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x_1.snd =
          ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x_1.fst) →
      (∃ x,
          y * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x.snd =
            ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x.fst) →
        ∃ x_1,
          x * y * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x_1.snd =
            ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x_1.fst
[PROOFSTEP]
rintro y z ⟨a, ha⟩ ⟨b, hb⟩
[GOAL]
case refine_4.intro.intro
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x : CyclotomicField n K
this : NeZero ↑↑n := NeZero.nat_of_injective (IsFractionRing.injective A K)
y z : CyclotomicField n K
a : CyclotomicRing n A K × { x // x ∈ nonZeroDivisors (CyclotomicRing n A K) }
ha :
  y * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.snd =
    ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) a.fst
b : CyclotomicRing n A K × { x // x ∈ nonZeroDivisors (CyclotomicRing n A K) }
hb :
  z * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.snd =
    ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) b.fst
⊢ ∃ x,
    y * z * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑x.snd =
      ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x.fst
[PROOFSTEP]
refine' ⟨⟨a.1 * b.1, a.2 * b.2, mul_mem_nonZeroDivisors.2 ⟨a.2.2, b.2.2⟩⟩, _⟩
[GOAL]
case refine_4.intro.intro
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x : CyclotomicField n K
this : NeZero ↑↑n := NeZero.nat_of_injective (IsFractionRing.injective A K)
y z : CyclotomicField n K
a : CyclotomicRing n A K × { x // x ∈ nonZeroDivisors (CyclotomicRing n A K) }
ha :
  y * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.snd =
    ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) a.fst
b : CyclotomicRing n A K × { x // x ∈ nonZeroDivisors (CyclotomicRing n A K) }
hb :
  z * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.snd =
    ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) b.fst
⊢ y * z *
      ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K))
        ↑(a.fst * b.fst,
              { val := ↑a.snd * ↑b.snd,
                property := (_ : ↑a.snd * ↑b.snd ∈ nonZeroDivisors (CyclotomicRing n A K)) }).snd =
    ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K))
      (a.fst * b.fst,
          { val := ↑a.snd * ↑b.snd, property := (_ : ↑a.snd * ↑b.snd ∈ nonZeroDivisors (CyclotomicRing n A K)) }).fst
[PROOFSTEP]
rw [RingHom.map_mul, mul_comm ((algebraMap (CyclotomicRing n A K) _) ↑a.2), mul_assoc, ← mul_assoc z, hb, ←
  mul_comm ((algebraMap (CyclotomicRing n A K) _) ↑a.2), ← mul_assoc, ha]
[GOAL]
case refine_4.intro.intro
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x : CyclotomicField n K
this : NeZero ↑↑n := NeZero.nat_of_injective (IsFractionRing.injective A K)
y z : CyclotomicField n K
a : CyclotomicRing n A K × { x // x ∈ nonZeroDivisors (CyclotomicRing n A K) }
ha :
  y * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑a.snd =
    ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) a.fst
b : CyclotomicRing n A K × { x // x ∈ nonZeroDivisors (CyclotomicRing n A K) }
hb :
  z * ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) ↑b.snd =
    ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) b.fst
⊢ ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) a.fst *
      ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) b.fst =
    ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K))
      (a.fst * b.fst,
          { val := ↑a.snd * ↑b.snd, property := (_ : ↑a.snd * ↑b.snd ∈ nonZeroDivisors (CyclotomicRing n A K)) }).fst
[PROOFSTEP]
simp only [map_mul]
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x y : CyclotomicRing n A K
h :
  ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x =
    ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) y
⊢ ↑1 * x = ↑1 * y
[PROOFSTEP]
rw [adjoin_algebra_injective n A K h]
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : Algebra A B
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : NeZero ↑↑n
x y : CyclotomicRing n A K
x✝ : ∃ c, ↑c * x = ↑c * y
c : { x // x ∈ nonZeroDivisors (CyclotomicRing n A K) }
hc : ↑c * x = ↑c * y
⊢ ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) x =
    ↑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) y
[PROOFSTEP]
rw [mul_left_cancel₀ (nonZeroDivisors.ne_zero c.prop) hc]
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
μ : CyclotomicField n K
h : IsPrimitiveRoot μ ↑n
⊢ CyclotomicRing n A K = { x // x ∈ adjoin A {μ} }
[PROOFSTEP]
rw [← IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic h,
  IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots h]
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
μ : CyclotomicField n K
h : IsPrimitiveRoot μ ↑n
⊢ CyclotomicRing n A K = { x // x ∈ adjoin A {b | ∃ a, a ∈ {n} ∧ b ^ ↑a = 1} }
[PROOFSTEP]
simp [CyclotomicRing]
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsAlgClosed K
h : ∀ (a : ℕ+), a ∈ S → NeZero ↑↑a
⊢ IsCyclotomicExtension S K K
[PROOFSTEP]
refine' ⟨@fun a ha => _, Algebra.eq_top_iff.mp <| Subsingleton.elim _ _⟩
[GOAL]
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsAlgClosed K
h : ∀ (a : ℕ+), a ∈ S → NeZero ↑↑a
a : ℕ+
ha : a ∈ S
⊢ ∃ r, IsPrimitiveRoot r ↑a
[PROOFSTEP]
obtain ⟨r, hr⟩ := IsAlgClosed.exists_aeval_eq_zero K _ (degree_cyclotomic_pos a K a.pos).ne'
[GOAL]
case intro
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsAlgClosed K
h : ∀ (a : ℕ+), a ∈ S → NeZero ↑↑a
a : ℕ+
ha : a ∈ S
r : K
hr : ↑(aeval r) (cyclotomic (↑a) K) = 0
⊢ ∃ r, IsPrimitiveRoot r ↑a
[PROOFSTEP]
refine' ⟨r, _⟩
[GOAL]
case intro
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsAlgClosed K
h : ∀ (a : ℕ+), a ∈ S → NeZero ↑↑a
a : ℕ+
ha : a ∈ S
r : K
hr : ↑(aeval r) (cyclotomic (↑a) K) = 0
⊢ IsPrimitiveRoot r ↑a
[PROOFSTEP]
haveI := h a ha
[GOAL]
case intro
n : ℕ+
S T : Set ℕ+
A : Type u
B : Type v
K : Type w
L : Type z
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsAlgClosed K
h : ∀ (a : ℕ+), a ∈ S → NeZero ↑↑a
a : ℕ+
ha : a ∈ S
r : K
hr : ↑(aeval r) (cyclotomic (↑a) K) = 0
this : NeZero ↑↑a
⊢ IsPrimitiveRoot r ↑a
[PROOFSTEP]
rwa [coe_aeval_eq_eval, ← IsRoot.def, isRoot_cyclotomic_iff] at hr 
