diff options
| author | thery | 2020-10-04 14:44:41 +0200 |
|---|---|---|
| committer | thery | 2020-10-10 15:47:22 +0200 |
| commit | 96a540fcd58dd37ef464a89ac7dc6f5cb7e2dd65 (patch) | |
| tree | bc6d227b251ff8148e5994b8850e957edd936bdd /mathcomp/algebra/ssrnum.v | |
| parent | eb47a0a031efab69f9a39c8cf356e2304c1e318f (diff) | |
Adding bigop lemmas for ring : expr_sum and prodr_natmul
Diffstat (limited to 'mathcomp/algebra/ssrnum.v')
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 2ebbdcc..974c81e 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -3435,7 +3435,7 @@ have [m leAm] := ubnP #|A|; elim: m => // m IHm in A leAm E n * => Ege0. apply/leifP; case: ifPn => [/forall_inP-Econstant | Enonconstant]. have [i /= Ai | A0] := pickP (mem A); last by rewrite [n]eq_card0 ?big_pred0. have /eqfun_inP-E_i := Econstant i Ai; rewrite -(eq_bigr _ E_i) sumr_const. - by rewrite exprMn_n prodrMn -(eq_bigr _ E_i) prodr_const. + by rewrite exprMn_n prodrMn_const -(eq_bigr _ E_i) prodr_const. set mu := \sum_(i in A) E i; pose En i := E i *+ n. pose cmp_mu s := [pred i | s * mu < s * En i]. have{Enonconstant} has_cmp_mu e (s := (-1) ^+ e): {i | i \in A & cmp_mu s i}. @@ -3468,7 +3468,7 @@ have ->: \sum_(k in A') E' k = mu *+ n'. apply: (addrI mu); rewrite -mulrS -Dn -sumrMnl (bigD1 i Ai) big_andbC /=. rewrite !(bigD1 j A'j) /= addrCA eqxx !addrA subrK; congr (_ + _). by apply: eq_bigr => k /andP[_ /negPf->]. -rewrite prodrMn exprMn_n -/n' ler_pmuln2r ?expn_gt0; last by case: (n'). +rewrite prodrMn_const exprMn_n -/n' ler_pmuln2r ?expn_gt0; last by case: (n'). have ->: \prod_(k in A') E' k = E' j * pi. by rewrite (bigD1 j) //=; congr *%R; apply: eq_bigr => k /andP[_ /negPf->]. rewrite -(ler_pmul2l mu_gt0) -exprS -Dn mulrA; apply: lt_le_trans. |