Merge pull request #474 from llelf/doc-typos

Documentation typos

mathcomp/algebra/matrix.v

@@ -100,7 +100,7 @@ From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg.
 (*         \adj A == the adjugate matrix of A (\adj A i j = cofactor j i A).  *)
 (*   A \in unitmx == A is invertible (R must be a comUnitRingType).           *)
 (*        invmx A == the inverse matrix of A if A \in unitmx A, otherwise A.  *)
-(* The following operations provide a correspondance between linear functions *)
+(* The following operations provide a correspondence between linear functions *)
 (* and matrices:                                                              *)
 (*     lin1_mx f == the m x n matrix that emulates via right product          *)
 (*                  a (linear) function f : 'rV_m -> 'rV_n on ROW VECTORS     *)
@@ -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.           *)
@@ -1837,7 +1837,7 @@ Lemma mulmx_block m1 m2 n1 n2 p1 p2 (Aul : 'M_(m1, n1)) (Aur : 'M_(m1, n2))
                (Adl *m Bul + Adr *m Bdl) (Adl *m Bur + Adr *m Bdr).
 Proof. by rewrite mul_col_mx !mul_row_block. Qed.
 
-(* Correspondance between matrices and linear function on row vectors. *) 
+(* Correspondence between matrices and linear function on row vectors. *)
 Section LinRowVector.
 
 Variables m n : nat.
@@ -1856,7 +1856,7 @@ Qed.
 
 End LinRowVector.
 
-(* Correspondance between matrices and linear function on matrices. *) 
+(* Correspondence between matrices and linear function on matrices. *)
 Section LinMatrix.
 
 Variables m1 n1 m2 n2 : nat.
@@ -1959,7 +1959,7 @@ by congr (_ + _); apply: eq_bigr => i _; rewrite (block_mxEul, block_mxEdr).
 Qed.
 
 (* The matrix ring structure requires a strutural condition (dimension of the *)
-(* form n.+1) to statisfy the nontriviality condition we have imposed.        *)
+(* form n.+1) to satisfy the nontriviality condition we have imposed.         *)
 Section MatrixRing.
 
 Variable n' : nat.

mathcomp/algebra/poly.v

@@ -10,7 +10,7 @@ From mathcomp Require Import fintype bigop div ssralg countalg binomial tuple.
 (*                                                                            *)
 (*           {poly R} == the type of polynomials with coefficients of type R, *)
 (*                       represented as lists with a non zero last element    *)
-(*                       (big endian representation); the coeficient type R   *)
+(*                       (big endian representation); the coefficient type R  *)
 (*                       must have a canonical ringType structure cR. In fact *)
 (*                       {poly R} denotes the concrete type polynomial cR; R  *)
 (*                       is just a phantom argument that lets type inference  *)

mathcomp/character/integral_char.v

@@ -83,7 +83,7 @@ Qed.
 Section GenericClassSums.
 
 (* This is Isaacs, Theorem (2.4), generalized to an arbitrary field, and with *)
-(* the combinatorial definition of the coeficients exposed.                   *)
+(* the combinatorial definition of the coefficients exposed.                  *)
 (* This part could move to mxrepresentation.*)
 
 Variable (gT : finGroupType) (G : {group gT}) (F : fieldType).

mathcomp/character/mxabelem.v

@@ -11,7 +11,7 @@ From mathcomp Require Import mxalgebra mxrepresentation.
 (******************************************************************************)
 (*   This file completes the theory developed in mxrepresentation.v with the  *)
 (* construction and properties of linear representations over finite fields,  *)
-(* and in particular the correspondance between internal action on a (normal) *)
+(* and in particular the correspondence between internal action on a (normal) *)
 (* elementary abelian p-subgroup and a linear representation on an Fp-module. *)
 (*   We provide the following next constructions for a finite field F:        *)
 (*        'Zm%act == the action of {unit F} on 'M[F]_(m, n).                  *)

mathcomp/field/algnum.v

@@ -17,7 +17,7 @@ From mathcomp Require Import cyclotomic.
 (*  x \in Cint_span X <=> x is a Z-linear combination of elements of          *)
 (*                        X : seq algC.                                       *)
 (*         x \in Aint <=> x : algC is an algebraic integer, i.e., the (monic) *)
-(*                        polynomial of x over Q has integer coeficients.     *)
+(*                        polynomial of x over Q has integer coefficients.    *)
 (*         (e %| a)%A <=> e divides a with respect to algebraic integers,     *)
 (*        (e %| a)%Ax     i.e., a is in the algebraic integer ideal generated *)
 (*                        by e. This is is notation for a \in dvdA e, where   *)

mathcomp/ssreflect/bigop.v

@@ -5,12 +5,12 @@ From mathcomp Require Import div fintype tuple finfun.
 
 (******************************************************************************)
 (* This file provides a generic definition for iterating an operator over a   *)
-(* set of indices (bigop); this big operator is parametrized by the return    *)
+(* set of indices (bigop); this big operator is parameterized by the return   *)
 (* type (R), the type of indices (I), the operator (op), the default value on *)
 (* empty lists (idx), the range of indices (r), the filter applied on this    *)
 (* range (P) and the expression we are iterating (F). The definition is not   *)
 (* to be used directly, but via the wide range of notations provided and      *)
-(* and which support a natural use of big operators.                          *)
+(* which support a natural use of big operators.                              *)
 (*   To improve performance of the Coq typechecker on large expressions, the  *)
 (* bigop constant is OPAQUE. It can however be unlocked to reveal the         *)
 (* transparent constant reducebig, to let Coq expand summation on an explicit *)
@@ -27,7 +27,7 @@ From mathcomp Require Import div fintype tuple finfun.
 (*  2. Results depending on the properties of the operator:                   *)
 (*     We distinguish: monoid laws (op is associative, idx is an identity     *)
 (*     element), abelian monoid laws (op is also commutative), and laws with  *)
-(*     a distributive operation (semi-rings). Examples of such results are    *)
+(*     a distributive operation (semirings). Examples of such results are     *)
 (*     splitting, permuting, and exchanging bigops.                           *)
 (* A special section is dedicated to big operators on natural numbers.        *)
 (******************************************************************************)

mathcomp/ssreflect/binomial.v

@@ -5,10 +5,10 @@ From mathcomp Require Import div fintype tuple finfun bigop prime finset.
 
 (******************************************************************************)
 (* This files contains the definition of:                                     *)
-(*   'C(n, m) == the binomial coeficient n choose m.                          *)
+(*   '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   *)

mathcomp/ssreflect/eqtype.v

@@ -38,7 +38,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool.
 (*         x != y :> T <=> x and y compare unequal at type T.                 *)
 (*             x =P y  :: a proof of reflect (x = y) (x == y); x =P y coerces *)
 (*                     to x == y -> x = y.                                    *)
-(*               eq_op == the boolean relation behing the == notation.        *)
+(*               eq_op == the boolean relation behind the == notation.        *)
 (*             pred1 a == the singleton predicate [pred x | x == a].          *)
 (* pred2, pred3, pred4 == pair, triple, quad predicates.                      *)
 (*            predC1 a == [pred x | x != a].                                  *)
@@ -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] ==                                *)
@@ -73,7 +73,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool.
 (*                insub x = Some u with val u = x if P x,                     *)
 (*                          None if ~~ P x                                    *)
 (*             The insubP lemma encapsulates this dichotomy.                  *)
-(*             P should be infered from the expected return type.             *)
+(*             P should be inferred from the expected return type.            *)
 (*  innew x == total (non-option) variant of insub when P = predT.            *)
 (* {? x | P} == option {x | P} (syntax for casting insub x).                  *)
 (* insubd u0 x == the generic projection with default value u0.               *)
@@ -92,7 +92,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool.
 (*   [subType for S_val by Srect], [newType for S_val by Srect]               *)
 (*     variants of the above where the eliminator is explicitly provided.     *)
 (*     Here S no longer needs to be syntactically identical to {x | P x} or   *)
-(*     wrapped T, but it must have a derived constructor S_Sub statisfying an *)
+(*     wrapped T, but it must have a derived constructor S_Sub satisfying an  *)
 (*     eliminator Srect identical to the one the Coq Inductive command would  *)
 (*     have generated, and S_val (S_Sub x Px) (resp. S_val (S_sub x) for the  *)
 (*     newType form) must be convertible to x.                                *)
@@ -437,7 +437,7 @@ End Endo.
 
 Variable aT : Type.
 
-(* The invariant of an function f wrt a projection k is the pred of points *)
+(* The invariant of a function f wrt a projection k is the pred of points  *)
 (* that have the same projection as their image.                           *)
 
 Definition invariant (rT : eqType) f (k : aT -> rT) :=

mathcomp/ssreflect/finfun.v

@@ -39,7 +39,7 @@ From mathcomp Require Import fintype tuple.
 (*                     limitations referred to above.                         *)
 (*        ffun0 aT0 == the trivial finfun, from a proof aT0 that #|aT| = 0.   *)
 (*   f \in family F == f belongs to the family F (f x \in F x for all x)      *)
-(*   There are addidional operations for non-dependent finite functions,      *)
+(*   There are additional operations for non-dependent finite functions,      *)
 (* i.e., f in {ffun aT -> rT}.                                                *)
 (*    [ffun x => E] := finfun (fun x => E).                                   *)
 (*                     The type of E must not depend on x; this restriction   *)
@@ -155,7 +155,7 @@ Proof. by fix IHt 2 => n [st]; apply/Kstep=> i; apply: IHt. Defined.
 Set Elimination Schemes.
 (* End example. *) *)
 
-(* The correspondance between finfun_of and CiC dependent functions.          *)
+(* The correspondence between finfun_of and CiC dependent functions.          *)
 Section DepPlainTheory.
 Variables (aT : finType) (rT : aT -> Type).
 Notation fT := {ffun finPi aT rT}.

mathcomp/ssreflect/fingraph.v

@@ -776,7 +776,7 @@ Qed.
 (* has to apply it to the natural numbers corresponding to the line, e.g.    *)
 (* `orbitPcycle 0 2 : fcycle f (orbit x) <-> exists k, iter k.+1 f x = x`.   *)
 (* examples of this are in order_id_cycle and fconnnect_f.                   *)
-(* One may also use lemma all_iffLR to get a one sided impliciation, as in   *)
+(* One may also use lemma all_iffLR to get a one sided implication, as in    *)
 (* orderPcycle.                                                              *)
 (*****************************************************************************)
 Lemma orbitPcycle {x} : [<->

mathcomp/ssreflect/finset.v

@@ -43,7 +43,7 @@ From mathcomp Require Import choice fintype finfun bigop.
 (*    is_transversal X P D <=> X is a transversal of the partition P of D.    *)
 (*   transversal P D == a transversal of P, provided P is a partition of D.   *)
 (*  transversal_repr x0 X B == a representative of B \in P selected by the    *)
-(*                      tranversal X of P, or else x0.                        *)
+(*                      transversal X of P, or else x0.                       *)
 (*        powerset A == the set of all subset of the set A.                   *)
 (*          P ::&: A == those sets in P that are subsets of the set A.        *)
 (*         f @^-1: A == the preimage of the collective predicate A under f.   *)
@@ -56,7 +56,7 @@ From mathcomp Require Import choice fintype finfun bigop.
 (*  [set E | x in A, y in B] == the set of values of E for x drawn from A and *)
 (*                      and y drawn from B; B may depend on x.                *)
 (*  [set E | x <- A, y <- B & P] == the set of values of E for x drawn from A *)
-(*                      y drawn from B, such that P is trye.                  *)
+(*                      y drawn from B, such that P is true.                  *)
 (*  [set E | x : T] == the set of all values of E, with x in type T.          *)
 (*  [set E | x : T & P] == the set of values of E for x : T s.t. P is true.   *)
 (*  [set E | x : T, y : U in B], [set E | x : T, y : U in B & P],             *)
@@ -102,7 +102,7 @@ From mathcomp Require Import choice fintype finfun bigop.
 (* These suffixes are sometimes preceded with an `s' to distinguish them from *)
 (* their basic ssrbool interpretation, e.g.,                                  *)
 (*  card1 : #|pred1 x| = 1 and cards1 : #|[set x]| = 1                        *)
-(* We also use a trailling `r' to distinguish a right-hand complement from    *)
+(* We also use a trailing `r' to distinguish a right-hand complement from     *)
 (* commutativity, e.g.,                                                       *)
 (*  setIC : A :&: B = B :&: A and setICr : A :&: ~: A = set0.                 *)
 (******************************************************************************)
@@ -146,7 +146,7 @@ Notation "{ 'set' T }" := (set_of (Phant T))
 (* preferable to state equalities at the {set _} level, even when comparing   *)
 (* subtype values, because the primitive "injection" tactic tends to diverge  *)
 (* on complex types (e.g., quotient groups). We provide some parse-only       *)
-(* notation to make this technicality less obstrusive.                        *)
+(* notation to make this technicality less obstructive.                       *)
 Notation "A :=: B" := (A = B :> {set _})
   (at level 70, no associativity, only parsing) : set_scope.
 Notation "A :<>: B" := (A <> B :> {set _})
@@ -2128,7 +2128,7 @@ Qed.
 
 (**********************************************************************)
 (*                                                                    *)
-(*  Maximum and minimun (sub)set with respect to a given pred         *)
+(*  Maximum and minimum (sub)set with respect to a given pred         *)
 (*                                                                    *)
 (**********************************************************************)
 

mathcomp/ssreflect/fintype.v

@@ -108,7 +108,7 @@ From mathcomp Require Import path.
 (*     invF inj_f y == the x such that f x = y, for inj_j : injective f with  *)
 (*                     f : T -> T.                                            *)
 (*  dinjectiveb A f <=> the restriction of f : T -> R to A is injective       *)
-(*                     (this is a bolean predicate, R must be an eqType).     *)
+(*                     (this is a boolean predicate, R must be an eqType).    *)
 (*     injectiveb f <=> f : T -> R is injective (boolean predicate).          *)
 (*         pred0b A <=> no x : T satisfies x \in A.                           *)
 (*    [forall x, P] <=> P (in which x can appear) is true for all values of x *)

mathcomp/ssreflect/generic_quotient.v

@@ -10,7 +10,7 @@ From mathcomp Require Import seq fintype.
 (* provide a helper to quotient T by a decidable equivalence relation (e     *)
 (* : rel T) if T is a choiceType (or encodable as a choiceType modulo e).    *)
 (*                                                                           *)
-(* See "Pragamatic Quotient Types in Coq", proceedings of ITP2013,           *)
+(* See "Pragmatic Quotient Types in Coq", proceedings of ITP2013,            *)
 (* by Cyril Cohen.                                                           *)
 (*                                                                           *)
 (* *** Generic Quotienting ***                                               *)
@@ -263,7 +263,7 @@ Hypothesis pi_r : {mono \pi : x y / r x y >-> rq x y}.
 Hypothesis pi_h : forall (x : T), \pi_qU (h x) = hq (\pi_qT x).
 Variables (a b : T) (x : equal_to (\pi_qT a)) (y : equal_to (\pi_qT b)).
 
-(* Internal Lemmmas : do not use directly *)
+(* Internal Lemmas : do not use directly *)
 Lemma pi_morph1 : \pi (f a) = fq (equal_val x). Proof. by rewrite !piE. Qed.
 Lemma pi_morph2 : \pi (g a b) = gq (equal_val x) (equal_val y). Proof. by rewrite !piE. Qed.
 Lemma pi_mono1 : p a = pq (equal_val x). Proof. by rewrite !piE. Qed.
@@ -294,7 +294,7 @@ Notation PiMono2 pi_r :=
 Notation PiMorph11 pi_f :=
   (fun a (x : {pi a}) => EqualTo (pi_morph11 pi_f a x)).
 
-(* lifiting helpers *)
+(* lifting helpers *)
 Notation lift_op1 Q f := (locked (fun x : Q => \pi_Q (f (repr x)) : Q)).
 Notation lift_op2 Q g := 
   (locked (fun x y : Q => \pi_Q (g (repr x) (repr y)) : Q)).