pointwiseZero

Mathlib.Algebra.Module.Submodule.Pointwise

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

English

There is a canonical Zero instance on submodules given by the bottom submodule.

Русский

Существует канонический нулевой инстанс для подмодуля, задаваемый нижним подмодулем.

LaTeX

$$$\text{pointwiseZero}: Zero (Submodule\ R\ M)$ with\ zero := ⊥$$

Lean4

instance pointwiseZero : Zero (Submodule R M) where zero := ⊥

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

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

Разделы

Аффилиация

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