of_union_of_dvd — Mathlib

English

Let n be a nonzero natural, and S a subset of natural numbers. If there exists s in S with s ≠ 0 and n divides s, then IsCyclotomicExtension S A B implies IsCyclotomicExtension (S ∪ {n}) A B.

Русский

Пусть n — ненулевое натуральное число, S — подмножество ℕ. Если существует 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 \\Rightarrow IsCyclotomicExtension (S \\cup \\{n\\}) A B \\right)$$$

Lean4

/-- If there exists a nonzero `s ∈ S` such that `n ∣ s`, then `IsCyclotomicExtension S A B`
implies `IsCyclotomicExtension (S ∪ {n}) A B`. -/
theorem of_union_of_dvd (h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s) [H : IsCyclotomicExtension S A B] :
    IsCyclotomicExtension (S ∪ { n }) A B :=
  by
  refine (iff_adjoin_eq_top _ A _).2 ⟨fun s hs hs' ↦ ?_, ?_⟩
  · rw [mem_union, mem_singleton_iff] at hs
    obtain hs | rfl := hs
    · exact H.exists_isPrimitiveRoot hs hs'
    · obtain ⟨m, hm, hm', ⟨x, rfl⟩⟩ := h
      obtain ⟨ζ, hζ⟩ := H.exists_isPrimitiveRoot hm hm'
      refine ⟨ζ ^ x, ?_⟩
      have h_xnz : x ≠ 0 := Nat.ne_zero_of_mul_ne_zero_right hm'
      have := hζ.pow_of_dvd h_xnz (dvd_mul_left x s)
      rwa [mul_div_cancel_right₀ _ h_xnz] at this
  · refine _root_.eq_top_iff.2 ?_
    rw [← ((iff_adjoin_eq_top S 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, hm, hm'⟩ := hx
    exact ⟨m, ⟨Or.inr hm, hm'⟩⟩

Похожие утверждения