absNorm_eq_zero_iff — Mathlib

English

AbsNorm vanishes exactly when the ideal is zero; absNorm I = 0 iff I = ⊥.

Русский

AbsNorm обращается в ноль тогда, когда идеал равен нулю; absNorm I = 0 iff I = ⊥.

LaTeX

$$absNorm(I) = 0 ↔ I = ⊥$$

Lean4

theorem absNorm_eq_zero_iff {I : Ideal S} : Ideal.absNorm I = 0 ↔ I = ⊥ :=
  by
  constructor
  · intro hI
    rw [← le_bot_iff]
    intro x hx
    rw [mem_bot, ← Algebra.norm_eq_zero_iff (R := ℤ), ← Int.natAbs_eq_zero, ← Ideal.absNorm_span_singleton, ←
      zero_dvd_iff, ← hI]
    apply Ideal.absNorm_dvd_absNorm_of_le
    rwa [Ideal.span_singleton_le_iff_mem]
  · rintro rfl
    exact absNorm_bot

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