absNorm_eq' — Mathlib

English

If a ∈ R⁰ and I₀ is an ideal with a I = map I₀, then absNorm(I) = absNorm(I₀)/|norm(a)|.

Русский

Если a ∈ R⁰ и I₀ такой, что a I = map I₀, то absNorm(I) = absNorm(I₀) / |norm(a)|.

LaTeX

$$absNorm(I) = (Ideal.absNorm I₀) / |\\operatorname{norm} (a)|$$

Lean4

theorem absNorm_eq' {I : FractionalIdeal R⁰ K} (a : R⁰) (I₀ : Ideal R)
    (h : a • (I : Submodule R K) = Submodule.map (Algebra.linearMap R K) I₀) :
    absNorm I = (Ideal.absNorm I₀ : ℚ) / |Algebra.norm ℤ (a : R)| := by
  rw [absNorm, ← absNorm_div_norm_eq_absNorm_div_norm a I₀ h, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]

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