Unique additive inverse (LADR 1.27)

• Unique additive inverse (LADR 1.27) #Card
  • ベクトル空間の各元の加法逆元は一意か？ 証明の鍵は？

Back

命題. ベクトル空間の各元は一意な加法逆元をもつ。

証明. $v\in V$ の逆元を $w,w’$ とすると $$w=w+0=w+(v+w’)=(w+v)+w’=0+w’=w’.$$ よって $w=w’$。一意性ゆえ記号 $-v$（および $w-v:=w+(-v)$）が意味をもつ (1.28)。

Lean

加法群で neg_unique 相当。逆元は Neg により定まり add_left_neg/neg_eq_of_add_eq_zero で特徴づく。