linearEquivFunOnFintype_symm_coe — Mathlib

English

The symm of the linear equivalence acts as the identity on the direct sum: (linearEquivFunOnFintype R ι M).symm f = f.

Русский

Обратное линейного эквивалентного отображения действует как тождественное на прямой сумме: (linearEquivFunOnFintype R ι M).symm f = f.

LaTeX

$$$ (linearEquivFunOnFintype\\; R\\; ι\\; M).symm\\; f = f $$$

Lean4

@[simp]
theorem linearEquivFunOnFintype_symm_coe [Fintype ι] (f : ⨁ i, M i) : (linearEquivFunOnFintype R ι M).symm f = f :=
  (linearEquivFunOnFintype R ι M).symm_apply_apply _

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