git.iko.soy/Idris-dev
on master help sign in
Fixed typo, removed some extra whitespace
commit19cb950678aaf02050741555119f51b59c588fad authorBlackBrane <cs.hbar@gmail.com> dateTue 4 Nov 2014, 13:15 (12 years ago) parente612c84
2 files changed+1−4
compare with master
unifiedsplit
libs/base/Data/Matrix.idr−3 libs/prelude/Prelude/Algebra.idr+1−1
libs/base/Data/Matrix.idr−3
@@ -66,7 +66,6 @@ instance RingWithUnity a => Module a (Vect n (Vect l a)) where
6666basis : RingWithUnity a => {d : Nat} -> (Fin d) -> Vect d a
6767basis i = replaceAt i unity $ neutral
6868
69−
7069-----------------------------------------------------------------------
7170-- Matrix functions
7271-----------------------------------------------------------------------
@@ -138,12 +137,10 @@ Id {d} = map (\n => basis n) $ allN d
138137(>><<) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
139138(>><<) m1 m2 = (m1 <> m2) <+> (m2 <> m1)
140139
141−
142140-----------------------------------------------------------------------
143141-- Matrix Algebra Properties
144142-----------------------------------------------------------------------
145143
146−
147144-- TODO: Prove properties of matrix algebra for 'Verified' algebraic classes
148145
149146-----------------------------------------------------------------------
libs/prelude/Prelude/Algebra.idr+1−1
@@ -299,7 +299,7 @@ class (VerifiedRing a, Field a) => VerifiedField a where
299299 total fieldInverseIsInverseL : (l : a) -> l <*> inverseM l = unity
300300 total fieldInverseIsInverseR : (r : a) -> inverseM r <*> r = unity
301301
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
303303||| scale operation multiplying vectors by ring elements, and distributivity laws
304304||| relating the scale operation to both ring addition and module addition.
305305||| Must satisfy the following laws: