mk₀_addEquiv₀_apply — Mathlib

English

The additive equivalence addEquiv₀ aligns with mk₀ on sums, i.e., addEquiv₀(f + g) corresponds to the sum of addEquiv₀ f and addEquiv₀ g under theHAdd operation.

Русский

Аддитивная эквивалентность addEquiv₀ согласуется с mk₀ на суммах: addEquiv₀(f+g) соответствует сумме addEquiv₀ f и addEquiv₀ g.

LaTeX

$$$\\mathrm{addEquiv}_0(\\alpha+\\beta) = \\mathrm{addEquiv}_0(\\alpha) + \\mathrm{addEquiv}_0(\\beta)$$$

Lean4

@[simp]
theorem mk₀_addEquiv₀_apply (f : Ext X Y 0) : mk₀ (addEquiv₀ f) = f :=
  addEquiv₀.left_inv f

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