absNorm_ne_zero_of_nonZeroDivisors

Mathlib.RingTheory.Ideal.Norm.AbsNorm

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem absNorm_ne_zero_of_nonZeroDivisors (I : (Ideal S)⁰) : absNorm (I : Ideal S) ≠ 0 :=
  absNorm_ne_zero_iff_mem_nonZeroDivisors.mpr (SetLike.coe_mem I)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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