English
Let n be nonzero. If there exists s ∈ S with s ≠ 0 and n ∣ s, then IsCyclotomicExtension S A B holds iff IsCyclotomicExtension (S ∪ {n}) A B holds.
Русский
Пусть n ≠ 0. Если найдётся s ∈ S с s ≠ 0 и n делит s, то IsCyclotomicExtension S A B эквивалентно IsCyclotomicExtension (S ∪ {n}) A B.
LaTeX
$$$\\left(\\exists s \\in S\\, (s \\neq 0 \\wedge n \\mid s)\\right) \\Rightarrow \\left(IsCyclotomicExtension S A B \\iff IsCyclotomicExtension(S \\cup \\{n\\}) A B\\right)$$$
Lean4
/-- If there exists a nonzero `s ∈ S` such that `n ∣ s`, then `IsCyclotomicExtension S A B`
if and only if `IsCyclotomicExtension (S ∪ {n}) A B`. -/
theorem iff_union_of_dvd (h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s) :
IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ { n }) A B :=
by
refine ⟨fun H ↦ of_union_of_dvd A B h, fun H => (iff_adjoin_eq_top _ A _).2 ⟨fun s hs ↦ ?_, ?_⟩⟩
· exact H.exists_isPrimitiveRoot (subset_union_left hs)
· rw [_root_.eq_top_iff, ← ((iff_adjoin_eq_top _ A B).1 H).2]
refine adjoin_mono fun x hx => ?_
simp only [union_singleton, mem_insert_iff, mem_setOf_eq] at hx ⊢
obtain ⟨m, rfl | hm, hxpow⟩ := hx
· obtain ⟨y, ⟨hy, hy', ⟨z, rfl⟩⟩⟩ := h
exact ⟨_, ⟨hy, hy', by simp only [pow_mul, hxpow, one_pow]⟩⟩
· exact ⟨m, ⟨hm, hxpow⟩⟩
