top_isPrincipal

Mathlib.RingTheory.PrincipalIdealDomain

URI: https://scilib.ai/kg/mathlib#top_isPrincipal

English

The top submodule ⊤ is principal.

Русский

Верхний подмодуль ⊤ — главный.

LaTeX

$$(\top : Submodule R R).IsPrincipal$$

Lean4

instance top_isPrincipal : (⊤ : Submodule R R).IsPrincipal :=
  ⟨⟨1, Ideal.span_singleton_one.symm⟩⟩

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

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

Разделы

Аффилиация

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