Unique additive identity (LADR 1.26)

• Unique additive identity (LADR 1.26) #Card
  • ベクトル空間の加法単位元は一意か？ 証明の鍵は？

Back

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

証明. $0,0’$ をともに加法単位元とすると $$0’=0’+0=0+0’=0,$$ （第1の等号は $0$ が単位元、第2は可換律、第3は $0’$ が単位元）。よって $0’=0$。

Lean

加法群で add_zero / zero_add から従う標準事実。AddZeroClass の単位元は型として一意。