spanNorm_eq

Mathlib.RingTheory.Ideal.Norm.RelNorm

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

English

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

Русский

Для Дедекендовых доменов R и S выполняется: relNorm(I) = ⊥ тогда и только тогда, когда I = ⊥.

LaTeX

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

Lean4

@[simp]
theorem spanNorm_eq (I : Ideal S) : spanNorm R I = relNorm R I :=
  rfl

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

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

Разделы

Аффилиация

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