isPrincipalIdealRing_of_isPrincipal_of_norm_le

English

If every ideal I in (𝓞_K)⁰ with absNorm(I) ≤ M(K) is principal, then 𝓞_K is a Principal Ideal Ring.

Русский

Если каждый идеал I над 𝓞_K с absNorm(I) ≤ M(K) является Principal, тогда 𝓞_K — кольцо главных идеалов.

LaTeX

$$$\left( \forall I:\; (I\subseteq (\mathcal{O}_K))^{\circ},\; \mathrm{absNorm}(I) \le M(K) \Rightarrow \mathrm{Submodule.IsPrincipal}(I) \right) \Rightarrow \mathrm{IsPrincipalIdealRing}(\mathcal{O}_K)$$$

Lean4

theorem isPrincipalIdealRing_of_isPrincipal_of_norm_le
    (h : ∀ ⦃I : (Ideal (𝓞 K))⁰⦄, absNorm (I : Ideal (𝓞 K)) ≤ M K → Submodule.IsPrincipal (I : Ideal (𝓞 K))) :
    IsPrincipalIdealRing (𝓞 K) :=
  by
  rw [← classNumber_eq_one_iff, classNumber, Fintype.card_eq_one_iff]
  refine ⟨1, fun C ↦ ?_⟩
  obtain ⟨I, rfl, hI⟩ := exists_ideal_in_class_of_norm_le C
  simpa [← ClassGroup.mk0_eq_one_iff] using h hI

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