fix typos in documentation: formulae

4 files changed, 4 insertions, 4 deletions

diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index dfdaf8b..f49473f 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -129,7 +129,7 @@ From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg.
 (* - The Cramer rule : mul_mx_adj & mul_adj_mx.                               *)
 (* Finally, as an example of the use of block products, we program and prove  *)
 (* the correctness of a classical linear algebra algorithm:                   *)
-(*    cormenLUP A == the triangular decomposition (L, U, P) of a nontrivial   *)
+(*   cormen_lup A == the triangular decomposition (L, U, P) of a nontrivial   *)
 (*                   square matrix A into a lower triagular matrix L with 1s  *)
 (*                   on the main diagonal, an upper matrix U, and a           *)
 (*                   permutation matrix P, such that P * A = L * U.           *)
diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v
index 2af7953..aef8e27 100644
--- a/mathcomp/ssreflect/binomial.v
+++ b/mathcomp/ssreflect/binomial.v
@@ -8,7 +8,7 @@ From mathcomp Require Import div fintype tuple finfun bigop prime finset.
 (*   'C(n, m) == the binomial coefficient n choose m.                         *)
 (*     n ^_ m == the falling (or lower) factorial of n with m terms, i.e.,    *)
 (*               the product n * (n - 1) * ... * (n - m + 1).                 *)
-(*               Note that n ^_ m = 0 if m > n, and 'C(n, m) = n ^_ m %/ m/!. *)
+(*               Note that n ^_ m = 0 if m > n, and 'C(n, m) = n ^_ m %/ m`!. *)
 (*                                                                            *)
 (* In additions to the properties of these functions, we prove a few seminal  *)
 (* results such as triangular_sum, Wilson and Pascal; their proofs are good   *)
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 296f85e..6832ea7 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -47,7 +47,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool.
 (*  predU1 a P, predD1 P a == applicative versions of the above.              *)
 (*              frel f == the relation associated with f : T -> T.            *)
 (*                     := [rel x y | f x == y].                               *)
-(*       invariant k f == elements of T whose k-class is f-invariant.         *)
+(*       invariant f k == elements of T whose k-class is f-invariant.         *)
 (*                     := [pred x | k (f x) == k x] with f : T -> T.          *)
 (*  [fun x : T => e0 with a1 |-> e1, .., a_n |-> e_n]                         *)
 (*  [eta f with a1 |-> e1, .., a_n |-> e_n] ==                                *)
diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v
index ed55b08..c682a20 100644
--- a/mathcomp/ssreflect/tuple.v
+++ b/mathcomp/ssreflect/tuple.v
@@ -18,7 +18,7 @@ Unset Printing Implicit Defensive.
 (* [tuple x1; ..; xn] == the explicit n.-tuple <x1; ..; xn>.                  *)
 (*  [tuple E | i < n] == the n.-tuple with general term E (i : 'I_n is bound  *)
 (*                       in E).                                               *)
-(*        tcast Emn t == the m-tuple t cast as an n-tuple using Emn : m = n.  *)
+(*        tcast Emn t == the m.-tuple t cast as an n-tuple using Emn : m = n. *)
 (* As n.-tuple T coerces to seq t, all seq operations (size, nth, ...) can be *)
 (* applied to t : n.-tuple T; we provide a few specialized instances when     *)
 (* avoids the need for a default value.                                       *)