aboutsummaryrefslogtreecommitdiff
path: root/mathcomp
diff options
context:
space:
mode:
authorFlorent Hivert2016-11-16 21:38:28 +0100
committerFlorent Hivert2016-11-16 21:38:28 +0100
commit5daf14d44b9cd22c6b51b2b23b4eebe5f3aee79f (patch)
tree4d0bd30c4f69f775afb53cb983a13b7b4c6e5c45 /mathcomp
parent8c704cf7eaddd1858113e46ea00a79e094b102db (diff)
Fixes the doc of mxalgebra
Diffstat (limited to 'mathcomp')
-rw-r--r--mathcomp/algebra/mxalgebra.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index 38dc17d..a0fa1c6 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -93,7 +93,7 @@ Require Import perm zmodp matrix.
(* capmx_gen A B is a rectangular matrix equivalent to *)
(* (A :&: B)%MS, i.e., (capmx_gen A B == A :&: B)%MS. *)
(* proj_mx A B == a square matrix that projects (A + B)%MS onto A *)
-(* parellel to B, when (A :&: B)%MS = 0 (A and B must also *)
+(* parallel to B, when (A :&: B)%MS = 0 (A and B must also *)
(* be square). *)
(* mxdirect S == the sum expression S is a direct sum. This is a NON *)
(* EXTENSIONAL notation: the exact boolean expression is *)