instZero

Mathlib.Data.Holor

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

English

Reiterates that Holor α ds inherits a zero element when α has one.

Русский

Повторное утверждение, что Holor наследует ноль от α, если у α есть ноль.

LaTeX

$$[Same as previous: Holor.instZero under different context]$$

Lean4

instance [Zero α] : Zero (Holor α ds) :=
  ⟨fun _ => 0⟩

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

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

Разделы

Аффилиация

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