d_squared_apply — Mathlib

English

The differential on a differential object squares to zero: for every x, X.d x ≫ X.d (some successor) = 0

Русский

Дифференциал у дифференциального объекта квадратируется в ноль: для всякого x выполняется X.d x ∘ X.d (следующий) = 0.

LaTeX

$$$\forall x,\; X.d x \;\circ\; X.d (\text{succ}(x)) = 0$$$

Lean4

@[reassoc (attr := simp)]
theorem d_squared_apply {x : β} : X.d x ≫ X.d _ = 0 :=
  congr_fun X.d_squared
    _
      -- Removing `@[simp]`, because it is in the opposite direction of `eqToHom_naturality`.
      -- Having both causes an infinite loop in the simpNF linter.

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