top_asIdeal

Mathlib.RingTheory.TwoSidedIdeal.Operations

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem top_asIdeal : (⊤ : TwoSidedIdeal R).asIdeal = ⊤ :=
  rfl

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

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

Разделы

Аффилиация

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