diff options
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 8 | ||||
| -rw-r--r-- | mathcomp/algebra/poly.v | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 0725885..dfdaf8b 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 *) @@ -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 *) |