English
IsCyclotomicExtension S A B is equivalent to IsCyclotomicExtension (S ∪ {1}) A B for all S, A, B under suitable algebraic structure.
Русский
IsCyclotomicExtension S A B эквивалентно IsCyclotomicExtension (S ∪ {1}) A B при надлежащей алгебраической структуре.
LaTeX
$$$IsCyclotomicExtension S A B \\iff IsCyclotomicExtension(S \\cup \\{1\\}) A B$$$
Lean4
/-- `IsCyclotomicExtension S A B` is equivalent to `IsCyclotomicExtension (S ∪ {1}) A B`. -/
theorem iff_union_singleton_one : IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ { 1 }) A B :=
by
by_cases hS : ∃ s ∈ S, s ≠ 0
· exact iff_union_of_dvd _ _ (by simpa)
· rw [eq_self_sdiff_zero S, eq_self_sdiff_zero (S ∪ { 1 }), union_diff_distrib, show S \ {0} = ∅ by aesop,
empty_union, show { 1 } \ {0} = { 1 } by simp]
refine ⟨fun H ↦ ?_, fun H ↦ ?_⟩
· refine (iff_adjoin_eq_top _ A _).2 ⟨fun s hs _ ↦ ⟨1, by simp [mem_singleton_iff.1 hs]⟩, ?_⟩
simpa [adjoin_singleton_one] using subsingleton_iff_bot_eq_top.mpr inferInstance
· refine (iff_adjoin_eq_top _ A _).2 ⟨fun s hs ↦ (notMem_empty s hs).elim, ?_⟩
simp [singleton_one]
