absNorm_eq

Mathlib.RingTheory.FractionalIdeal.Norm

URI: https://scilib.ai/kg/mathlib#FractionalIdeal.absNorm_eq

English

For any fractional ideal I, absNorm(I) equals (Ideal.absNorm I.num) / |Algebra.norm ℤ (I.den)|.

Русский

Для дробного идеала I нормa absNorm(I) равна (Ideal.absNorm I.num) / |Algebra.norm ℤ (I.den)|.

LaTeX

$$absNorm(I) = \\frac{\\operatorname{absNorm}(I.num)}{|\\operatorname{norm} (I.den)|}$$

Lean4

theorem absNorm_eq (I : FractionalIdeal R⁰ K) : absNorm I = (Ideal.absNorm I.num : ℚ) / |Algebra.norm ℤ (I.den : R)| :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru