relNorm_bot

Mathlib.RingTheory.Ideal.Norm.RelNorm

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

English

The relative norm sends the bottom ideal to bottom: relNorm_R(⊥) = ⊥.

Русский

Относительная норма отображает нулевой идеал в нулевой идеал: relNorm_R(⊥) = ⊥.

LaTeX

$$$\mathrm{relNorm}_R(\bot) = \bot$$$

Lean4

@[simp]
theorem relNorm_bot : relNorm R (⊥ : Ideal S) = ⊥ := by
  simpa only [zero_eq_bot] using map_zero (relNorm R : Ideal S →*₀ _)

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

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

Разделы

Аффилиация

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