English
If IsDomain B and IsCyclotomicExtension {n} A B, then Module.Finite A B.
Русский
Если B — область, и IsCyclotomicExtension {n} A B, то B является конечным как модуль над A.
LaTeX
$$[IsDomain B] [h : IsCyclotomicExtension { n } A B] ⇒ Module.Finite A B$$
Lean4
theorem finite_of_singleton [IsDomain B] [h : IsCyclotomicExtension { n } A B] : Module.Finite A B := by
classical
rw [Module.finite_def, ← top_toSubmodule, ← ((iff_adjoin_eq_top _ _ _).1 h).2]
refine fg_adjoin_of_finite ?_ fun b ⟨n, hb⟩ => ?_
· simp only [mem_singleton_iff, exists_eq_left]
have : {b : B | n ≠ 0 ∧ b ^ n = 1} = (nthRoots n (1 : B)).toFinset :=
Set.ext fun x ↦
⟨fun h ↦ by simpa [n.pos_of_neZero] using h.2, fun h ↦ by simpa [n.pos_of_neZero, NeZero.ne n] using h⟩
rw [this]
exact (nthRoots n 1).toFinset.finite_toSet
· simp only [mem_singleton_iff] at hb
exact ⟨X ^ n - 1, ⟨monic_X_pow_sub_C _ (hb.1 ▸ NeZero.ne _), by simpa [sub_eq_zero] using hb.2.2⟩⟩
