diff options
| author | Florent Hivert | 2019-11-14 15:57:35 +0100 |
|---|---|---|
| committer | Assia Mahboubi | 2019-11-14 15:57:35 +0100 |
| commit | 03dc3079d231817a99cb896c3cd264792c568514 (patch) | |
| tree | 5c37b5ddc8115c71c10227bf780ce94701b2a637 | |
| parent | 521e80b0729baa445c2c1884f5f96d594deda0c8 (diff) | |
Lemmas on commutation with big sum and prod (#413)
* Lemmas on commutation with big sum and prod
* Added commrB Lemma
* @CohenCyril review
* apply -> apply:
| -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. |