mkHom_f_0 — Mathlib

English

Another expression for the law giving the (n+2)-th component of mkHom in terms of the previous ones via succ.

Русский

Ещё одно выражение закона для (n+2)-й компоненты mkHom через предыдущие с помощью succ.

LaTeX

$$$$(\\mathrm{mkHom})_{n+2} = \\text{succ } n (\\mathrm{mkHom}_n, \\mathrm{mkHom}_{n+1}, \\mathrm{comm}) .1$$$$

Lean4

@[simp]
theorem mkHom_f_0 : (mkHom P Q zero one one_zero_comm succ).f 0 = zero :=
  rfl

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