zero_def

Mathlib.GroupTheory.OreLocalization.Basic

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

English

The equation defining the zero fraction: (0 : X[S⁻¹]) = 0 /ₒ 1.

Русский

Уравнение определения нулевой дроби: (0 : X[S⁻¹]) = 0 /ₒ 1.

LaTeX

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

Lean4

protected theorem zero_def : (0 : X[S⁻¹]) = 0 /ₒ 1 := by with_unfolding_all rfl

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

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

Разделы

Аффилиация

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