Merge pull request #474 from llelf/doc-typos

Documentation typos

2 files changed, 6 insertions, 6 deletions

diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index 0725885..f49473f 100644
--- a/mathcomp/algebra/matrix.v
+++ b/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.
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index e25d7c0..d21e690 100644
--- a/mathcomp/algebra/poly.v
+++ b/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  *)