coe_zero

Mathlib.Algebra.Order.Nonneg.Basic

URI: https://scilib.ai/kg/mathlib#Nonneg.coe_zero

English

The zero element of the ambient ring maps to zero in the nonnegative substructure under the coercion.

Русский

Ноль кольца отображается в ноль внутри подпредмета при коэрции.

LaTeX

$$$((0 : { x : α // 0 ≤ x }) : α) = 0$$$

Lean4

@[simp, norm_cast]
protected theorem coe_zero [Zero α] [Preorder α] : ((0 : { x : α // 0 ≤ x }) : α) = 0 :=
  rfl

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

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

Разделы

Аффилиация

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