Rename MultNeutral to MultGroup

src/Data/NumIdr/Homogeneous.idr

@@ -99,11 +99,11 @@ getTranslationVector mat with (viewShape mat)
 
 
 export
-scalingH : Num a => {n : _} -> a -> HMatrix' n a
+scalingH : {n : _} -> Num a => a -> HMatrix' n a
 scalingH x = indexSet [last,last] 1 $ repeatDiag x 0
 
 export
-translationH : Num a => {n : _} -> Vector n a -> HMatrix' n a
+translationH : {n : _} -> Num a => Vector n a -> HMatrix' n a
 translationH = hmatrix identity
 
 export

src/Data/NumIdr/Matrix.idr

@@ -59,15 +59,9 @@ fromDiag ds o = fromFunction [m,n] (\[i,j] => maybe o (`index` ds) $ i `eq` j)
     eq (FS _) FZ = Nothing
 
 
-||| The `n`-dimensional identity matrix.
-export
-identity : Num a => {n : _} -> Matrix' n a
-identity = repeatDiag 1 0
-
-
 ||| Construct the matrix that scales a vector by the given value.
 export
-scaling : Num a => {n : _} -> a -> Matrix' n a
+scaling : {n : _} -> Num a => a -> Matrix' n a
 scaling x = repeatDiag x 0
 
 ||| Calculate the rotation matrix of an angle.
@@ -157,5 +151,7 @@ Num a => Mult (Matrix m n a) (Matrix n p a) (Matrix m p a) where
         (\k => m1 !! [i,k] * m2 !! [k,j]) range)
 
 export
-{n : _} -> Num a => MultNeutral (Matrix' n a) where
-  neutral = identity
+{n : _} -> Num a => MultGroup (Matrix' n a) where
+  identity = repeatDiag 1 0
+
+  inverse = ?matrixInverse

src/Data/NumIdr/Multiply.idr

@@ -16,32 +16,40 @@ public export
 interface Mult a b c | a,b where
   (*.) : a -> b -> c
 
-||| An interface for monoids using the `*.` operator.
+public export
+Mult' : Type -> Type
+Mult' a = Mult a a a
+
+
+||| An interface for groups using the `*.` operator.
 |||
 ||| An instance of this interface must satisfy:
 ||| * `x *. neutral == x`
 ||| * `neutral *. x == x`
+||| * `x *. inverse x == neutral`
+||| * `inverse x *. x == neutral`
 public export
-interface Mult a a a => MultNeutral a where
-  neutral : a
+interface Mult' a => MultGroup a where
+  identity : a
+  inverse : a -> a
 
 
 ||| Multiplication forms a semigroup
 public export
-[MultSemigroup] Mult a a a => Semigroup a where
+[MultSemigroup] Mult' a => Semigroup a where
   (<+>) = (*.)
 
-||| Multiplication with a neutral element forms a monoid
+||| Multiplication with an identity element forms a monoid
 public export
-[MultMonoid] MultNeutral a => Monoid a using MultSemigroup where
-  neutral = Multiply.neutral
+[MultMonoid] MultGroup a => Monoid a using MultSemigroup where
+  neutral = identity
 
 
 ||| Raise a multiplicative value (e.g. a matrix or a transformation) to a natural
 ||| number power.
 public export
-power : MultNeutral a => Nat -> a -> a
-power 0 _ = neutral
+power : MultGroup a => Nat -> a -> a
+power 0 _ = identity
 power 1 x = x
 power (S n@(S _)) x = x *. power n x
 
@@ -50,5 +58,5 @@ power (S n@(S _)) x = x *. power n x
 |||
 ||| This is the operator form of `power`.
 public export
-(^) : MultNeutral a => a -> Nat -> a
+(^) : MultGroup a => a -> Nat -> a
 (^) = flip power