diff options
| author | Antonio Nikishaev | 2020-04-05 02:54:23 +0400 |
|---|---|---|
| committer | Antonio Nikishaev | 2020-04-08 01:13:13 +0400 |
| commit | 815d3cbfa2bf98b4b8f2bcd14819a20eca843e78 (patch) | |
| tree | d3564d7ccb62b38493fde1a0fc23ff94410074ec /mathcomp/algebra/matrix.v | |
| parent | 14e28e78155e3e6cfbe78aee0964569283f04d7d (diff) | |
fix typos in documentation: text
Diffstat (limited to 'mathcomp/algebra/matrix.v')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 8 |
1 files changed, 4 insertions, 4 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. |