eq_bot_iff_generator_eq_zero

Mathlib.RingTheory.PrincipalIdealDomain

URI: https://scilib.ai/kg/mathlib#Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero

← MathLib Explorer

English

For a principal submodule S, S = ⊥ iff generator S = 0.

Русский

Для главного подмодуля S выполняется S = ⊥ тогда и только тогда, когда generator S = 0.

LaTeX

$$S = ⊥ ⇔ generator S = 0$$

Lean4

theorem eq_bot_iff_generator_eq_zero (S : Submodule R M) [S.IsPrincipal] : S = ⊥ ↔ generator S = 0 := by
  rw [← @span_singleton_eq_bot R M, span_singleton_generator]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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