diff options
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/matrix.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 5e42904..e7e0e35 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -112,7 +112,7 @@ From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg. (* A \is a mxOver S == the matrix A has its coefficients in S. *) (* comm_mx A B := A *m B = B *m A *) (* comm_mxb A B := A *m B == B *m A *) -(* all_comm_mx As fs := all1rel comm_mxb fs *) +(* all_comm_mx As fs := all2rel comm_mxb fs *) (* The following operations provide a correspondence between linear functions *) (* and matrices: *) (* lin1_mx f == the m x n matrix that emulates via right product *) @@ -2772,21 +2772,21 @@ Proof. by move=> comm_mxfF; elim/big_ind: _ => // g h; apply: comm_mxD. Qed. Lemma comm_mxP f g : reflect (comm_mx f g) (comm_mxb f g). Proof. exact: eqP. Qed. -Notation all_comm_mx fs := (all1rel comm_mxb fs). +Notation all_comm_mx fs := (all2rel comm_mxb fs). Lemma all_comm_mxP fs : reflect {in fs &, forall f g, f *m g = g *m f} (all_comm_mx fs). Proof. by apply: (iffP allrelP) => fsP ? ? ? ?; apply/eqP/fsP. Qed. Lemma all_comm_mx1 f : all_comm_mx [:: f]. -Proof. by rewrite /comm_mxb all1rel1. Qed. +Proof. by rewrite /comm_mxb all2rel1. Qed. Lemma all_comm_mx2P f g : reflect (f *m g = g *m f) (all_comm_mx [:: f; g]). -Proof. by rewrite /comm_mxb /= all1rel2 ?eqxx //; exact: eqP. Qed. +Proof. by rewrite /comm_mxb /= all2rel2 ?eqxx //; exact: eqP. Qed. Lemma all_comm_mx_cons f fs : all_comm_mx (f :: fs) = all (comm_mxb f) fs && all_comm_mx fs. -Proof. by rewrite /comm_mxb /= all1rel_cons //= eqxx. Qed. +Proof. by rewrite /comm_mxb /= all2rel_cons //= eqxx. Qed. End CommMx. Notation all_comm_mx := (allrel comm_mxb). |