git.iko.soy/Idris-dev
on master help sign in
Fixed typo, removed some extra whitespace
19cb950BlackBrane
libs/base/Data/Matrix.idr−3
compare with master
unifiedsplit
@@ -66,7 +66,6 @@ instance RingWithUnity a => Module a (Vect n (Vect l a)) where
66basis : RingWithUnity a => {d : Nat} -> (Fin d) -> Vect d a
66basis : RingWithUnity a => {d : Nat} -> (Fin d) -> Vect d a
67basis i = replaceAt i unity $ neutral
67basis i = replaceAt i unity $ neutral
68
68
69−
70-----------------------------------------------------------------------
69-----------------------------------------------------------------------
71-- Matrix functions
70-- Matrix functions
72-----------------------------------------------------------------------
71-----------------------------------------------------------------------
@@ -138,12 +137,10 @@ Id {d} = map (\n => basis n) $ allN d
138(>><<) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
137(>><<) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
139(>><<) m1 m2 = (m1 <> m2) <+> (m2 <> m1)
138(>><<) m1 m2 = (m1 <> m2) <+> (m2 <> m1)
140
139
141−
142-----------------------------------------------------------------------
140-----------------------------------------------------------------------
143-- Matrix Algebra Properties
141-- Matrix Algebra Properties
144-----------------------------------------------------------------------
142-----------------------------------------------------------------------
145
143
146−
147-- TODO: Prove properties of matrix algebra for 'Verified' algebraic classes
144-- TODO: Prove properties of matrix algebra for 'Verified' algebraic classes
148
145
149-----------------------------------------------------------------------
146-----------------------------------------------------------------------
libs/prelude/Prelude/Algebra.idr+1−1
@@ -299,7 +299,7 @@ class (VerifiedRing a, Field a) => VerifiedField a where
299 total fieldInverseIsInverseL : (l : a) -> l <*> inverseM l = unity
299 total fieldInverseIsInverseL : (l : a) -> l <*> inverseM l = unity
300 total fieldInverseIsInverseR : (r : a) -> inverseM r <*> r = unity
300 total fieldInverseIsInverseR : (r : a) -> inverseM r <*> r = unity
301
301
302−||| A module over a ring is an additive abeliean group of 'vectors' endowed with a
302+||| A module over a ring is an additive abelian group of 'vectors' endowed with a
303||| scale operation multiplying vectors by ring elements, and distributivity laws
303||| scale operation multiplying vectors by ring elements, and distributivity laws
304||| relating the scale operation to both ring addition and module addition.
304||| relating the scale operation to both ring addition and module addition.
305||| Must satisfy the following laws:
305||| Must satisfy the following laws: