English
Nonzero fractional ideals contain a nonzero integer: there exists a ≠ 0 with a ∈ the fractional ideal after mapping from R to the fraction field.
Русский
Дробные идеалы, отличные от нуля, содержат ненулевой целый элемент при отображении в дробный элемент.
LaTeX
$$$\\exists x \, (x \\neq 0) \\land \\ algebraMap\\ R K\\ x \\in I$$$
Lean4
/-- Nonzero fractional ideals contain a nonzero integer. -/
theorem exists_ne_zero_mem_isInteger [Nontrivial R] (hI : I ≠ 0) : ∃ x, x ≠ 0 ∧ algebraMap R K x ∈ I :=
by
obtain ⟨y : K, y_mem, y_notMem⟩ := SetLike.exists_of_lt (by simpa only using bot_lt_iff_ne_bot.mpr hI)
have y_ne_zero : y ≠ 0 := by simpa using y_notMem
obtain ⟨z, ⟨x, hx⟩⟩ := exists_integer_multiple R⁰ y
refine ⟨x, ?_, ?_⟩
· rw [Ne, ← @IsFractionRing.to_map_eq_zero_iff R _ K, hx, Algebra.smul_def]
exact mul_ne_zero (IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors z.2) y_ne_zero
· rw [hx]
exact smul_mem _ _ y_mem
