sumFinsuppLEquivProdFinsupp_symm_inr

English

The inverse under the symmetrized equivalence sends the right injection coordinate back to the right component.

Русский

Обратное преобразование разворачивает правую инъекцию обратно к правой компоненте.

LaTeX

$$((sumFinsuppLEquivProdFinsupp R).symm f) (Sum.inr y) = f.2 y$$

Lean4

theorem sumFinsuppLEquivProdFinsupp_symm_inr {α β : Type*} (fg : (α →₀ M) × (β →₀ M)) (y : β) :
    ((sumFinsuppLEquivProdFinsupp R).symm fg) (Sum.inr y) = fg.2 y :=
  rfl

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