instZero

Mathlib.Algebra.Module.LocalizedModule.Basic

URI: https://scilib.ai/kg/mathlib#LocalizedModule.instZero

English

There is a zero element in the localized module given by the class of (0,1).

Русский

В локализованном модуле существует ноль, задаваемый классом (0,1).

LaTeX

$$$0_{\\text{Loc}} = \\text{mk}(0,1).$$$

Lean4

instance : Zero (LocalizedModule S M) :=
  ⟨mk 0 1⟩

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

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

Разделы

Аффилиация

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