slice_zero

Mathlib.Data.Holor

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

English

If 0 is taken as a Holor of shape d :: ds, then every i-th slice is zero.

Русский

Если рассматривать ноль как холор формы d :: ds, то каждый i-й срез равен нулю.

LaTeX

$$$$ \\operatorname{slice}(0 : \\operatorname{Holor}(\\alpha)(d :: ds))\\ i\\ hid = 0 $$$$

Lean4

theorem slice_zero [Zero α] (i : ℕ) (hid : i < d) : slice (0 : Holor α (d :: ds)) i hid = 0 :=
  rfl

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

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

Разделы

Аффилиация

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