English
Every nonzero ideal in a finite-dimensional setting contains a nonzero element of minimal norm with respect to the given admissible absolute value.
Русский
В каждом ненулевом идеале в конечномерной настройке существует минимальная по норме ненулевая элемент.
LaTeX
$$∃ b ∈ I, b ≠ 0 ∧ ∀ c ∈ I, abv(Algebra.norm R c) < abv(Algebra.norm R b) → c = 0$$
Lean4
/-- A nonzero ideal has an element of minimal norm. -/
theorem exists_min (I : (Ideal S)⁰) :
∃ b ∈ (I : Ideal S), b ≠ 0 ∧ ∀ c ∈ (I : Ideal S), abv (Algebra.norm R c) < abv (Algebra.norm R b) → c = (0 : S) :=
by
obtain ⟨_, ⟨b, b_mem, b_ne_zero, rfl⟩, min⟩ :=
@Int.exists_least_of_bdd (fun a => ∃ b ∈ (I : Ideal S), b ≠ (0 : S) ∧ abv (Algebra.norm R b) = a)
(by
use 0
rintro _ ⟨b, _, _, rfl⟩
apply abv.nonneg)
(by
obtain ⟨b, b_mem, b_ne_zero⟩ := (I : Ideal S).ne_bot_iff.mp (nonZeroDivisors.coe_ne_zero I)
exact ⟨_, ⟨b, b_mem, b_ne_zero, rfl⟩⟩)
refine ⟨b, b_mem, b_ne_zero, ?_⟩
intro c hc lt
contrapose! lt with c_ne_zero
exact min _ ⟨c, hc, c_ne_zero, rfl⟩
