spanNorm_top

Mathlib.RingTheory.Ideal.Norm.RelNorm

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

English

spanNorm of the bottom ideal is bottom, and spanNorm of the top ideal is top.

Русский

spanNorm от нижнего идеала дает нижний, а от верхнего — верхний идеал.

LaTeX

$$$$\operatorname{spanNorm}(R, \bot) = \bot \quad\text{and}\quad \operatorname{spanNorm}(R, \top) = \top.$$$$

Lean4

@[simp]
theorem spanNorm_top : spanNorm R (⊤ : Ideal S) = ⊤ := by simp [← Ideal.span_singleton_one]

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

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

Разделы

Аффилиация

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