absNorm_eq_zero_iff — Mathlib

English

For any integral ideal I₀, absNorm of its fractional ideal extension equals the integral norm: absNorm (I₀ : FractionalIdeal R⁰ K) = Ideal.absNorm I₀.

Русский

Для целого идеала I₀ норма absNorm вдоль расширения равна интегральной норме: absNorm (I₀ : FractionalIdeal R⁰ K) = Ideal.absNorm I₀.

LaTeX

$$absNorm (I_0 : FractionalIdeal R⁰ K) = Ideal.absNorm I_0$$

Lean4

theorem absNorm_eq_zero_iff [NoZeroDivisors K] {I : FractionalIdeal R⁰ K} : absNorm I = 0 ↔ I = 0 :=
  by
  refine ⟨fun h ↦ zero_of_num_eq_bot zero_notMem_nonZeroDivisors ?_, fun h ↦ h ▸ absNorm_bot⟩
  rw [absNorm_eq, div_eq_zero_iff] at h
  refine Ideal.absNorm_eq_zero_iff.mp <| Nat.cast_eq_zero.mp <| h.resolve_right ?_
  simp [Algebra.norm_eq_zero_iff]

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