diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 12 | ||||
| -rw-r--r-- | mathcomp/algebra/matrix.v | 14 | ||||
| -rw-r--r-- | mathcomp/algebra/mxalgebra.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 5 |
4 files changed, 17 insertions, 16 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 57e5e28..e78d37d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -221,12 +221,12 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). boolean versions of matrix commutation, `comm_mx A B` is definitionally equal to `GRing.comm A B` when `A B : 'M_n.+1`, this is witnessed by the lemma `comm_mxE`. New notation `all_comm_mx` - stands for `allrel comm_mxb`. New lemmas `comm_mx_sym`, `comm_mx_refl`, - `comm_mx0`, `comm0mx`, `comm_mx1`, `comm1mx`, `comm_mxN`, `comm_mxN1`, - `comm_mxD`, `comm_mxB`, `comm_mx_sum`, `comm_mxP`, `all_comm_mxP`, - `all_comm_mx1`, `all_comm_mx2P`, `all_comm_mx_cons`, `comm_mxC`, and - `commCmx`. The common arguments of these lemmas `R` and `n` are - maximal implicits. + stands for `allrel comm_mxb`. New lemmas `comm_mx_sym`, + `comm_mx_refl`, `comm_mx0`, `comm0mx`, `comm_mx1`, `comm1mx`, + `comm_mxN`, `comm_mxN1`, `comm_mxD`, `comm_mxB`, `comm_mx_sum`, + `comm_mxP`, `all_comm_mxP`, `all_comm_mx1`, `all_comm_mx2P`, + `all_comm_mx_cons`, `comm_mx_scalar`, and `comm_scalar_mx`. The + common arguments of these lemmas `R` and `n` are maximal implicits. - in `seq.v`, added `in_mask`, `cons_subseq`, `undup_subseq`, `subset_maskP`. - in `fintype.v`, added `mask_enum_ord`. diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index f7d7730..77d2e4f 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -2889,11 +2889,11 @@ Qed. Lemma mul_mx_scalar m n a (A : 'M[R]_(m, n)) : A *m a%:M = a *: A. Proof. by rewrite scalar_mxC mul_scalar_mx. Qed. -Lemma comm_mxC n a (A : 'M[R]_n) : comm_mx A a%:M. +Lemma comm_mx_scalar n a (A : 'M[R]_n) : comm_mx A a%:M. Proof. by rewrite /comm_mx mul_mx_scalar mul_scalar_mx. Qed. -Lemma commCmx n a (A : 'M[R]_n) : comm_mx a%:M A. -Proof. exact/comm_mx_sym/comm_mxC. Qed. +Lemma comm_scalar_mx n a (A : 'M[R]_n) : comm_mx a%:M A. +Proof. exact/comm_mx_sym/comm_mx_scalar. Qed. Lemma mxtrace_mulC m n (A : 'M[R]_(m, n)) B : \tr (A *m B) = \tr (B *m A). @@ -3140,16 +3140,16 @@ End ComMatrix. Arguments lin_mul_row {R m n} u. Arguments lin_mulmx {R m n p} A. -Arguments comm_mxC {R n}. -Arguments commCmx {R n}. +Arguments comm_mx_scalar {R n}. +Arguments comm_scalar_mx {R n}. Arguments diag_mx_comm {R n}. Canonical matrix_finAlgType (R : finComRingType) n' := [finAlgType R of 'M[R]_n'.+1]. -Hint Resolve comm_mxC commCmx : core. +Hint Resolve comm_mx_scalar comm_scalar_mx : core. -Notation "@ 'scalar_mx_comm'" := (deprecate scalar_mx_comm comm_mxC) +Notation "@ 'scalar_mx_comm'" := (deprecate scalar_mx_comm comm_mx_scalar) (at level 10, only parsing) : fun_scope. Notation scalar_mx_comm := (@scalar_mx_comm _ _) (only parsing). diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index e65bc3c..7aa89b8 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.v @@ -2291,7 +2291,7 @@ Lemma comm_mx_stable_eigenspace (f g : 'M[F]_n) a : comm_mx f g -> stablemx (eigenspace f a) g. Proof. move=> cfg; rewrite comm_mx_stable_ker//. -by apply/comm_mx_sym/comm_mxB => //; apply:comm_mxC. +by apply/comm_mx_sym/comm_mxB => //; apply:comm_mx_scalar. Qed. End Commutation. diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index c7f8fb1..19a23e6 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -274,7 +274,7 @@ Section OneMatrix. Variable A : 'M[R]_n. -Definition horner_mx := horner_morph (comm_mxC^~ A). +Definition horner_mx := horner_morph (comm_mx_scalar^~ A). Canonical horner_mx_additive := [additive of horner_mx]. Canonical horner_mx_rmorphism := [rmorphism of horner_mx]. @@ -317,7 +317,8 @@ Qed. Lemma comm_mx_horner A B p : comm_mx A B -> comm_mx A (horner_mx B p). Proof. -by move=> fg; apply: commr_horner => // i; rewrite coef_map; apply/commCmx. +move=> fg; apply: commr_horner => // i. +by rewrite coef_map; apply/comm_scalar_mx. Qed. Lemma comm_horner_mx A B p : comm_mx A B -> comm_mx (horner_mx A p) B. |