coeIdeal_absNorm — Mathlib

English

Another formulation: absNorm of the coeIdeal equals the usual integral norm.

Русский

Ещё одно формулирование: absNorm дробного идеала, полученного из целого идеала, равна обычной норме.

LaTeX

$$absNorm( (I_0) ) = Ideal.absNorm I_0$$

Lean4

theorem coeIdeal_absNorm (I₀ : Ideal R) : absNorm (I₀ : FractionalIdeal R⁰ K) = Ideal.absNorm I₀ := by
  rw [absNorm_eq' 1 I₀ (by rw [one_smul]; rfl), OneMemClass.coe_one, map_one, abs_one, Int.cast_one, _root_.div_one]

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