add_eq_sup

Mathlib.Algebra.Module.Submodule.Pointwise

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

English

The additive operation on submodules coincides with the lattice join.

Русский

Сложение подмодулей совпадает с объединением в решётке.

LaTeX

$$$p+q = p\sqcup q$$$

Lean4

@[simp]
theorem add_eq_sup (p q : Submodule R M) : p + q = p ⊔ q :=
  rfl

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

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

Разделы

Аффилиация

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