instZero

Mathlib.Algebra.Order.Ring.Archimedean

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

English

There exists a distinguished zero element in ArchimedeanClass R, given by mk 1.

Русский

Существует особый нуль в ArchimedeanClass R, задаваемый как mk 1.

LaTeX

$$$$ 0_{ArchimedeanClass(R)} = \operatorname{mk}(1). $$$$

Lean4

instance : Zero (ArchimedeanClass R) where zero := mk 1

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

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

Разделы

Аффилиация

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