diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 3 | ||||
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 14 |
2 files changed, 17 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c4906fc..0744c7c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -82,6 +82,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). of an algebra. The theory include the lemmas `in_alg_comm`, `horner_algC`, `horner_algX`, `poly_alg_initial`. +- Added lemmas on commutation with difference, big sum and prod: + `commrB`, `commr_sum`, `commr_prod`. + ### Changed - `eqVneq` lemma is changed from `{x = y} + {x != y}` to diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 0266dea..88920e0 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -1101,6 +1101,16 @@ Proof. exact/commrN/commr1. Qed. Lemma commrD x y z : comm x y -> comm x z -> comm x (y + z). Proof. by rewrite /comm mulrDl mulrDr => -> ->. Qed. +Lemma commrB x y z : comm x y -> comm x z -> comm x (y - z). +Proof. by move=> com_xy com_xz; apply: commrD => //; apply: commrN. Qed. + +Lemma commr_sum (I : Type) (s : seq I) (P : pred I) (F : I -> R) x : + (forall i, P i -> comm x (F i)) -> comm x (\sum_(i <- s | P i) F i). +Proof. +move=> comm_x_F; rewrite /comm mulr_suml mulr_sumr. +by apply: eq_bigr => i /comm_x_F. +Qed. + Lemma commrMn x y n : comm x y -> comm x (y *+ n). Proof. rewrite /comm => com_xy. @@ -1110,6 +1120,10 @@ Qed. Lemma commrM x y z : comm x y -> comm x z -> comm x (y * z). Proof. by move=> com_xy; rewrite /comm mulrA com_xy -!mulrA => ->. Qed. +Lemma commr_prod (I : Type) (s : seq I) (P : pred I) (F : I -> R) x : + (forall i, P i -> comm x (F i)) -> comm x (\prod_(i <- s | P i) F i). +Proof. exact: (big_ind _ (commr1 x) (@commrM x)). Qed. + Lemma commr_nat x n : comm x n%:R. Proof. exact/commrMn/commr1. Qed. |