coe_add — Mathlib

English

The coercion of the difference of cocycles equals the difference of their coerced cochains.

Русский

Приведение разности кокцикл равно разности их приведения к коцепам.

LaTeX

$$(↑(z1 - z2) : Cochain F G n) = (z1 : Cochain F G n) - (z2 : Cochain F G n)$$

Lean4

@[simp]
theorem coe_add (z₁ z₂ : Cocycle F G n) : (↑(z₁ + z₂) : Cochain F G n) = (z₁ : Cochain F G n) + (z₂ : Cochain F G n) :=
  rfl

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