add_eq — Mathlib

English

If two morphisms f1,f2 map to the same in the localized image, then their sum equals the sum defined by the isomorphisms eX,eY.

Русский

Если f1 и f2 совпадают в локализованном виде, их сумма равна сумме, определяемой изоморфизмами eX,eY.

LaTeX

$$$f_1,f_2:\\; X'\\to Y' \Rightarrow f_1 + f_2 = add\\; W\\; e_X\\; e_Y\\; f_1\\; f_2$$$

Lean4

theorem add_eq (f₁ f₂ : X' ⟶ Y') :
    letI := addCommGroup L W X' Y'
    f₁ + f₂ = add W eX eY f₁ f₂ :=
  by apply add_eq_add

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