absNorm_pos_of_nonZeroDivisors

Mathlib.RingTheory.Ideal.Norm.AbsNorm

URI: https://scilib.ai/kg/mathlib#Ideal.absNorm_pos_of_nonZeroDivisors

English

If I is a non-zero-divisor ideal, then absNorm(I) > 0.

Русский

Если I принадлежит множеству непустых делителей нуля, то absNorm(I) > 0.

LaTeX

$$$$I\in (\mathrm{Ideal}(S))^{0} \implies 0< \operatorname{absNorm}(I).$$$$

Lean4

theorem absNorm_pos_of_nonZeroDivisors (I : (Ideal S)⁰) : 0 < absNorm (I : Ideal S) :=
  absNorm_pos_iff_mem_nonZeroDivisors.mpr (SetLike.coe_mem I)

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

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

Разделы

Аффилиация

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