relNorm_eq_bot_iff

Mathlib.RingTheory.Ideal.Norm.RelNorm

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

English

For Dedekind domains, relNorm(I) = ⊥ if and only if I = ⊥.

Русский

Для Дедекендовых доменов верно: relNorm(I) = ⊥ эквивалентно I = ⊥.

LaTeX

$$$\mathrm{relNorm}(I) = \bot \iff I = \bot$$$

Lean4

@[simp]
theorem relNorm_eq_bot_iff {I : Ideal S} : relNorm R I = ⊥ ↔ I = ⊥ :=
  spanNorm_eq_bot_iff

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

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

Разделы

Аффилиация

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