pi_nil

Mathlib.Data.List.Pi

URI: https://scilib.ai/kg/mathlib#List.pi_nil

Lean4

@[simp]
theorem pi_nil (t : ∀ i, List (α i)) : pi [] t = [Pi.nil α] :=
  rfl

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

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

Разделы

Аффилиация

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