instMin

Mathlib.Algebra.Module.Submodule.Lattice

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

← MathLib Explorer

English

The meet operation on submodules is given by intersection: p ⊓ q = p ∩ q.

Русский

Операция meet над подмодулями равна их пересечению: p ∧ q = p ∩ q.

LaTeX

$$$p \wedge q = p \cap q$$$

Lean4

instance : Min (Submodule R M) :=
  ⟨fun p q ↦
    { carrier := p ∩ q
      zero_mem' := by simp [zero_mem]
      add_mem' := by simp +contextual [add_mem]
      smul_mem' := by simp +contextual [smul_mem] }⟩

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

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

Разделы

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

Аффилиация

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