bot_asIdeal

Mathlib.RingTheory.TwoSidedIdeal.Operations

URI: https://scilib.ai/kg/mathlib#TwoSidedIdeal.bot_asIdeal

English

The bottom two-sided ideal, when mapped via asIdeal, yields the bottom ideal.

Русский

Нижний двусторонний идеал при отображении через asIdeal превращается в нижний идеал.

LaTeX

$$$\big(\bot : TwoSidedIdeal(R)\big).asIdeal = \bot$$$

Lean4

@[simp]
theorem bot_asIdeal : (⊥ : TwoSidedIdeal R).asIdeal = ⊥ :=
  rfl

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

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

Разделы

Аффилиация

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