English
absNorm(under ℤ I) equals the infimum of natural numbers d>0 such that d cast to R lies in I.
Русский
absNorm(under ℤ I) равно наименьшему положительному натуральному числу d, для которого образ d в R принадлежит I.
LaTeX
$$$\operatorname{absNorm}(\operatorname{under} \mathbb{Z} I) = \operatorname{sInf} \{ d : \mathbb{N} \mid 0 < d \land (d : R) \in I \}$$$
Lean4
theorem absNorm_under_eq_sInf : absNorm (under ℤ I) = sInf {d : ℕ | 0 < d ∧ (d : R) ∈ I} :=
by
by_cases h : absNorm (under ℤ I) = 0
· have : {d : ℕ | 0 < d ∧ ↑d ∈ I} = ∅ :=
by
refine Set.eq_empty_of_forall_notMem ?_
intro x ⟨hx₁, hx₂⟩
rw [← cast_natCast, cast_mem_ideal_iff, h, natCast_dvd_natCast, Nat.zero_dvd] at hx₂
rw [Nat.pos_iff_ne_zero] at hx₁
exact hx₁ hx₂
rw [h, this, Nat.sInf_empty]
· have h₁ : absNorm (under ℤ I) ∈ {d : ℕ | 0 < d ∧ ↑d ∈ I} := ⟨Nat.pos_of_ne_zero h, absNorm_under_mem I⟩
refine le_antisymm ?_ (Nat.sInf_le h₁)
by_contra! h₀
have h₂ := (Nat.sInf_mem (Set.nonempty_of_mem h₁)).2
rw [← cast_natCast, cast_mem_ideal_iff, natCast_dvd_natCast] at h₂
exact lt_iff_not_ge.mp h₀ <| Nat.le_of_dvd (Nat.sInf_mem (Set.nonempty_of_mem h₁)).1 h₂
