Module とスカラー倍

「K を体，V を K ベクトル空間とする」は，Lean では次のように書きます．

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

[AddCommGroup V] と [Module K V] を分けて仮定するのは，型クラス探索を安定させるためです． スカラー倍は a • v と書き，補題名では smul と呼ばれます．

#check Module
#check SMul
#check smul_add
#check add_smul
#check smul_comm

section Modules

variable {K : Type*} [Field K]
variable {V : Type*} [AddCommGroup V] [Module K V]

example (a : K) (u v : V) : a • (u + v) = a • u + a • v := by
  exact smul_add a u v

example (a b : K) (u : V) : (a + b) • u = a • u + b • u := by
  exact add_smul a b u

example (a b : K) (u : V) : a • b • u = b • a • u := by
  exact smul_comm a b u

example (u : V) : (0 : K) • u = 0 := by
  simp

end Modules

module tactic は，加群の公理から従う等式を解くための tactic です． ring や group と同じく，構造の公理に沿った正規化を行います．

section ModuleTactic

variable {K : Type*} [Field K]
variable {V : Type*} [AddCommGroup V] [Module K V]

example (a b : K) (x y : V) : a • (x + y) + b • x = (a + b) • x + a • y := by
  module

end ModuleTactic