instZero

Mathlib.GroupTheory.OreLocalization.Basic

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

English

The localization carries a canonical zero element obtained from OreLocalization.zero.

Русский

Локализация наследует ноль, заданный через OreLocalization.zero.

LaTeX

$$$0_{X[S^{-1}]} = OreLocalization.zero$$$

Lean4

instance : Zero X[S⁻¹] :=
  ⟨OreLocalization.zero⟩

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

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

Разделы

Аффилиация

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