diff options
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 12 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 2 |
2 files changed, 6 insertions, 8 deletions
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index 078fea3..8d6c03b 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -2,7 +2,7 @@ (* Distributed under the terms of CeCILL-B. *) From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice. From mathcomp Require Import fintype finfun bigop finset fingroup perm. -From mathcomp Require Import div prime binomial ssralg finalg zmodp matrix. +From mathcomp Require Import div prime binomial ssralg finalg zmodp matrix. (*****************************************************************************) (* In this file we develop the rank and row space theory of matrices, based *) @@ -683,7 +683,7 @@ Qed. Lemma row_full_unit n (A : 'M_n) : row_full A = (A \in unitmx). Proof. exact: row_free_unit. Qed. - + Lemma mxrank_unit n (A : 'M_n) : A \in unitmx -> \rank A = n. Proof. by rewrite -row_full_unit => /eqnP. Qed. @@ -1488,7 +1488,7 @@ Proof. by rewrite unlock; apply/eqmxP; rewrite !genmxE !capmxE andbb. Qed. Lemma genmx_diff m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (<<A :\: B>> = A :\: B)%MS. Proof. by rewrite [@diffmx]unlock genmx_id. Qed. - + Lemma diffmxSl m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) : (A :\: B <= A)%MS. Proof. by rewrite diffmxE capmxSl. Qed. @@ -2202,7 +2202,7 @@ have p_i_gt0: p ^ _ > 0 by move=> i; rewrite expn_gt0 ltnW. rewrite (card_GL _ (ltn0Sn n.-1)) card_ord Fp_cast // big_add1 /=. pose p'gt0 m := m > 0 /\ logn p m = 0%N. suffices [Pgt0 p'P]: p'gt0 (\prod_(0 <= i < n.-1.+1) (p ^ i.+1 - 1))%N. - by rewrite lognM // p'P pfactorK //; case n. + by rewrite lognM // p'P pfactorK // addn0; case n. apply big_ind => [|m1 m2 [m10 p'm1] [m20]|i _]; rewrite {}/p'gt0 ?logn1 //. by rewrite muln_gt0 m10 lognM ?p'm1. rewrite lognE -if_neg subn_gt0 p_pr /= -{1 2}(exp1n i.+1) ltn_exp2r // p_gt1. @@ -2269,7 +2269,7 @@ by rewrite linear_sum; apply: eq_bigr => i _; rewrite mulmxKpV. Qed. Arguments memmx_sumsP {I P n A R_}. -Lemma has_non_scalar_mxP m n (R : 'A_(m, n)) : +Lemma has_non_scalar_mxP m n (R : 'A_(m, n)) : (1%:M \in R)%MS -> reflect (exists2 A, A \in R & ~~ is_scalar_mx A)%MS (1 < \rank R). Proof. @@ -2765,5 +2765,3 @@ Lemma map_center_mx m n (E : 'A_(m, n)) : (('Z(E))^f :=: 'Z(E^f))%MS. Proof. by rewrite /center_mx -map_cent_mx; apply: map_capmx. Qed. End MapMatrixSpaces. - - diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index 1b1eb77..3c4c002 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -1553,7 +1553,7 @@ Lemma abszN1 : `|-1%R| = 1. Proof. by []. Qed. Lemma absz_id m : `|(`|m|)| = `|m|. Proof. by []. Qed. Lemma abszM m1 m2 : `|(m1 * m2)%R| = `|m1| * `|m2|. -Proof. by case: m1 m2 => [[|m1]|m1] [[|m2]|m2]; rewrite //= mulnS mulnC. Qed. +Proof. by case: m1 m2 => [[|m1]|m1] [[|m2]|m2] //=; rewrite ?mulnS mulnC. Qed. Lemma abszX (n : nat) m : `|m ^+ n| = `|m| ^ n. Proof. by elim: n => // n ihn; rewrite exprS expnS abszM ihn. Qed. |