diff options
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 12 | ||||
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 7 | ||||
| -rw-r--r-- | mathcomp/algebra/poly.v | 2 |
3 files changed, 12 insertions, 9 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 0725885..21730c3 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. @@ -2395,7 +2395,7 @@ rewrite (reindex (lift_perm i0 j0)); last first. by rewrite lift_perm_lift -si0 permE ulsfK. rewrite /cofactor big_distrr /=. apply: eq_big => [s | s _]; first by rewrite lift_perm_id eqxx. -rewrite -signr_odd mulrA -signr_addb odd_add -odd_lift_perm; congr (_ * _). +rewrite -signr_odd mulrA -signr_addb oddD -odd_lift_perm; congr (_ * _). case: (pickP 'I_n) => [k0 _ | n0]; last first. by rewrite !big1 // => [j /unlift_some[i] | i _]; have:= n0 i. rewrite (reindex (lift i0)). diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index b39f600..a8cf94b 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -469,7 +469,7 @@ rewrite big_ord_recr big_ord_recl/= big1 ?add0r //=; last first. rewrite !mxE ?subnn -horner_coef0 /= hornerMXaddC. rewrite !(eqxx, mulr0, add0r, addr0, subr0, rmorphN, opprK)/=. rewrite mulrC /cofactor; congr (_ * 'X + _). - rewrite /cofactor -signr_odd odd_add addbb mul1r; congr (\det _). + rewrite /cofactor -signr_odd oddD addbb mul1r; congr (\det _). apply/matrixP => i j; rewrite !mxE -val_eqE coefD coefMX coefC. by rewrite /= /bump /= !add1n !eqSS addr0. rewrite /cofactor [X in \det X](_ : _ = D _). @@ -901,7 +901,10 @@ apply: integral_horner_root mon_p pu0 intRp _. by apply/integral_poly => i; rewrite coefX; apply: integral_nat. Qed. -Hint Resolve (integral0 RtoK) (integral1 RtoK) (@monicXsubC K) : core. +Let integral0_RtoK := integral0 RtoK. +Let integral1_RtoK := integral1 RtoK. +Let monicXsubC_K := @monicXsubC K. +Hint Resolve integral0_RtoK integral1_RtoK monicXsubC_K : core. Let XsubC0 (u : K) : root ('X - u%:P) u. Proof. by rewrite root_XsubC. Qed. Let intR_XsubC u : 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 *) |