prev_nat_zero

Mathlib.Algebra.Homology.HomologicalComplex

URI: https://scilib.ai/kg/mathlib#CochainComplex.prev_nat_zero

English

In the CochainComplex (up ℕ), prev 0 equals 0.

Русский

В CochainComplex (up ℕ) prev 0 равно 0.

LaTeX

$$$(\text{ComplexShape.up } \mathbb{N}).\text{prev } 0 = 0$$$

Lean4

@[simp]
theorem prev_nat_zero : (ComplexShape.up ℕ).prev 0 = 0 := by
  classical
  refine dif_neg ?_
  push_neg
  intro
  apply Nat.noConfusion

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

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

Разделы

Аффилиация

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