fix typos in documentation: formulae

3 files changed, 3 insertions, 3 deletions

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.                                       *)