zero

Mathlib.GroupTheory.OreLocalization.Basic

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

English

The zero element of the Ore localization is defined as the fraction 0 /ₒ 1.

Русский

Ноль локализации Оре задаётся дробью 0 /ₒ 1.

LaTeX

$$$0_{X[S^{-1}]} = 0 /_\\ o 1$$$

Lean4

/-- `0` in the localization, defined as `0 /ₒ 1`. -/
@[irreducible]
protected def zero : X[S⁻¹] :=
  0 /ₒ 1

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

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

Разделы

Аффилиация

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