absNorm_nonneg

Mathlib.RingTheory.FractionalIdeal.Norm

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

English

For any fractional ideal I, absNorm(I) is nonnegative.

Русский

Для любого дробного идеала I, absNorm(I) неотрицательна.

LaTeX

$$0 \\le absNorm(I)$$

Lean4

theorem absNorm_nonneg (I : FractionalIdeal R⁰ K) : 0 ≤ absNorm I := by dsimp [absNorm]; positivity

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

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

Разделы

Аффилиация

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