decomposeAlgEquiv_apply — Mathlib

English

Applying the algebraic decomposition map yields the same element as grouping through the direct sum decomposition.

Русский

Применение алгебраической декомпозиции даёт тот же элемент, что и разбиение через прямую сумму.

LaTeX

$$$ decomposeAlgEquiv 𝒜\; a = decompose 𝒜\; a.$$$

Lean4

@[simp]
theorem decomposeAlgEquiv_apply (a : A) : decomposeAlgEquiv 𝒜 a = decompose 𝒜 a :=
  rfl

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