Direct sum $\oplus$ (LADR 1.41)

• Direct sum $\oplus$ (LADR 1.41) #Card
  • 和 $V_1+\cdots+V_m$ が直和であるとは？ 記号は？

Back

和 $V_1+\cdots+V_m$ が直和であるとは、その各元が $v_1+\cdots+v_m$（$v_k\in V_k$）の形にただ一通りに書けること。 このとき和を $V_1\oplus\cdots\oplus V_m$ と書き、$\oplus$ が一意表現を示す。 直和は集合の「互いに素な合併」の類似物。

Lean

内部直和は DirectSum.IsInternal / Submodule.IsInternal。2つなら IsCompl U W （disjoint かつ codisjoint）。外部直和は ⨁ i, M i（DirectSum）。