decomposeLinearEquiv_symm_apply — Mathlib

English

The inverse isomorphism applied to a direct-sum element returns the corresponding sum in the original domain: (decomposeLinearEquiv ℳ).symm m = (decompose ℳ).symm m.

Русский

Обратное отображение возвращает исходный элемент: (decomposeLinearEquiv ℳ).symm m = (decompose ℳ).symm m.

LaTeX

$$$((\operatorname{decomposeLinearEquiv} \mathcal{M})^{\mathrm{symm}})(m) = (\operatorname{decompose} \mathcal{M})^{\mathrm{symm}}(m)$$$

Lean4

@[simp]
theorem decomposeLinearEquiv_symm_apply (m : ⨁ i, ℳ i) : (decomposeLinearEquiv ℳ).symm m = (decompose ℳ).symm m :=
  rfl

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