cast_mem_ideal_iff — Mathlib

English

For any ring R and ideal I, and any integer d, the element d in R lies in I if and only if absNorm(under ℤ I) divides d.

Русский

Для кольца R, идеала I и целого числа d выполняется: (d в R) ∈ I тогда и только тогда, когда absNorm(under ℤ I) делит d.

LaTeX

$$$\forall d \in \mathbb{Z},\ (d : R) \in I \iff (\operatorname{absNorm}(\operatorname{under} \mathbb{Z} I) : \mathbb{Z}) \mid d$$$

Lean4

theorem cast_mem_ideal_iff {d : ℤ} : (d : R) ∈ I ↔ (absNorm (under ℤ I) : ℤ) ∣ d := by
  rw [← mem_span_singleton, ideal_span_absNorm_eq_self, under_def, mem_comap, eq_intCast]

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