instAddCommGroupHom — Mathlib

English

For any M,N in ModuleCat, the set Hom(M,N) carries an AddCommGroup structure; in particular (f+g).hom = f.hom + g.hom, and 0 acts as the zero map.

Русский

Для любых модулей M,N в ModuleCat множество Hom(M,N) образует структуру AddCommGroup; например (f+g).hom = f.hom + g.hom, а ноль соответствует нулевому отображению.

LaTeX

$$$ (f+g)_{hom} = f_{hom} + g_{hom} $$$

Lean4

instance : AddCommGroup (M ⟶ N) :=
  Function.Injective.addCommGroup (Hom.hom) hom_injective rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) (fun _ _ => rfl)

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