restrictScalars_eq_bot_iff

Mathlib.Algebra.Module.Submodule.RestrictScalars

URI: https://scilib.ai/kg/mathlib#Submodule.restrictScalars_eq_bot_iff

English

Restriction to S of a submodule equals bottom iff the submodule is bottom.

Русский

Ограничение до S подмодуля равно нулю тогда и только тогда, когда подмодуль равен нулю.

LaTeX

$$$$ \\operatorname{restrictScalars}(S,p) = \\bot \\iff p = \\bot. $$$$

Lean4

@[simp]
theorem restrictScalars_eq_bot_iff {p : Submodule R M} : restrictScalars S p = ⊥ ↔ p = ⊥ := by simp [SetLike.ext_iff]

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

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

Разделы

Аффилиация

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