one_eq_top

Mathlib.RingTheory.Ideal.Operations

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

English

The unit ideal equals the top submodule: 1 = ⊤.

Русский

Единичный идеал равен верхнему подмодулю: 1 = ⊤.

LaTeX

$$$1 = \\top$$$

Lean4

@[simp, grind =]
theorem one_eq_top : (1 : Ideal R) = ⊤ := by rw [Submodule.one_eq_span, ← Ideal.span, Ideal.span_singleton_one]

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

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

Разделы

Аффилиация

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