instAddHom — Mathlib

English

For any X, Y in Action V G, the hom-set X ⟶ Y is equipped with an addition making it an additive structure.

Русский

Для любых X, Y в Action V G множество морфизмов X ⟶ Y оснащено дополнительной операцией сложения, образующей аддитивную структуру.

LaTeX

$$$\\operatorname{Add}(\\operatorname{Hom}_{Action}(X,Y))$$$

Lean4

instance : Add (X ⟶ Y) where add f g := ⟨f.hom + g.hom, by simp [f.comm, g.comm]⟩

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