norm_dvd_iff — Mathlib

English

For CharZero S, the set { I ∈ Ideal(S) | absNorm(I) ≤ n } is finite.

Русский

Для CharZero(S) множество { I ∈ Ideal(S) | absNorm(I) ≤ n } конечно.

LaTeX

$$$$\forall n\in \mathbb{N},\; { I \in \mathrm{Ideal}(S) \mid \operatorname{absNorm}(I) \le n \}.\Finite$$$$

Lean4

theorem norm_dvd_iff {x : S} (hx : Prime (Algebra.norm ℤ x)) {y : ℤ} : Algebra.norm ℤ x ∣ y ↔ x ∣ y :=
  by
  rw [← Ideal.mem_span_singleton (y := x), ← eq_intCast (algebraMap ℤ S), ← Ideal.mem_comap, ←
    Ideal.span_singleton_absNorm, Ideal.mem_span_singleton, Ideal.absNorm_span_singleton, Int.natAbs_dvd]
  rwa [Ideal.absNorm_span_singleton, ← Int.prime_iff_natAbs_prime]

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