isInternal — Mathlib

English

There exists a canonical additive isomorphism between the finite direct sum and the corresponding product of components.

Русский

Существует канонический аддитивный изоморфизм между конечной прямой суммой и соответствующим произведением компонент.

LaTeX

$$$\text{There exists a canonical additive isomorphism } DirectSum ι G \cong+ (i\mapsto G_i)$$$

Lean4

protected theorem isInternal : DirectSum.IsInternal ℳ :=
  ⟨Decomposition.right_inv.injective, Decomposition.left_inv.surjective⟩

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