egison-4.1.3: lib/math/geometry/differential-form.egi

def dfNormalize %X :=
  let p := dfOrder X
      (es, os) := evenAndOddPermutations p
   in withSymbols [i]
        (sum (map (\σ -> subrefs X (map 1#i_(σ %1) (between 1 p))) es)
       - sum (map (\σ -> subrefs X (map 1#i_(σ %1) (between 1 p))) os))
       / fact p

def antisymmetrize := dfNormalize

def wedge %X %Y := X !. Y

infixl expression 7 ∧

def (∧) := wedge

def Lie.wedge %X %Y := X !. Y - Y !. X

def ι %X %Y := withSymbols [i] dfOrder Y * (X...~i . dfNormalize Y..._i)

def Lie %X %Y :=
  match dfOrder Y as integer with
    | #0 -> ι X (d Y)
    | #N -> d (ι X Y)
    | _ -> ι X (d Y) + d (ι X Y)