homAddEquiv_symm_add — Mathlib

English

Symmetric additive equivalence respects addition on the symmetric side.

Русский

Симметрическое аддитивное соответствие сохраняет сложение на симметричной стороне.

LaTeX

$$((adj.homEquiv X Y).symm (f+g)) = ((adj.homEquiv X Y).symm f) + ((adj.homEquiv X Y).symm g)$$

Lean4

@[simp]
theorem homAddEquiv_symm_add (X : C) (Y : D) (f f' : X ⟶ G.obj Y) :
    (adj.homEquiv X Y).symm (f + f') = (adj.homEquiv X Y).symm f + (adj.homEquiv X Y).symm f' :=
  map_add (adj.homAddEquiv X Y).symm _ _

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