Advertisement
Guest User

Untitled

a guest
Nov 29th, 2019
199
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 2.17 KB | None | 0 0
  1. From mathcomp Require Import all_ssreflect all_algebra all_fingroup all_field.
  2.  
  3. Search Monoid.law.
  4. Locate Monoid.law.
  5. Section Agrawal.
  6. Variables (n':nat).
  7. Definition n : nat := n'.+2.
  8.  
  9. Open Scope ring_scope.
  10.  
  11. (*Lemma aux : forall (n : nat), prime n -> \sum_(1 <= i < n) (@polyC [ringType of {poly 'F_n}] 0) = (@polyC [ringType of {poly 'F_n}] 0).
  12. Proof.
  13. induction n0; first by move=> pn.
  14. move=> pn.
  15. rewrite big_nat_recr//=.
  16. rewrite GRing.addr0.
  17. admit.
  18. assert (n0.+1 >= 2)%N; first by exact: prime_gt1.
  19. by rewrite ltnSS.
  20. Admitted.
  21. *)
  22. Check [idomainType of 'F_n].
  23. Lemma EulerFermatPoly : forall (a : 'F_n), prime n -> (polyC a)^+n = polyC a.
  24. Admitted.
  25. Lemma agrawal_biswas: forall (a : 'F_n), prime n <-> (('X + a%:P)^+n = 'X^n + a%:P).
  26. Proof.
  27. move=> a; split.
  28. move=> pn.
  29. Search binomial.
  30. Search 'C(_,_) .
  31. rewrite GRing.exprDn.
  32. Search "rec" "big".
  33. move: (pn).
  34. move/prime_dvd_bin => n_dvd_coef.
  35. Check ( \sum_(i < n.+1) 'X^(n - i) * a%:P ^+ i *+ 'C(n, i)).
  36. Search "big_mkord".
  37. Locate "\sum_".
  38. Search bump.
  39. rewrite big_ord_recl//=.
  40.  
  41. rewrite bin0.
  42. rewrite big_ord_recr //=.
  43. rewrite subn0.
  44. rewrite GRing.expr0 GRing.mulr1 GRing.mulr1n //=.
  45. rewrite/bump//=.
  46. rewrite(_ : (1 + n'.+1 = n)%N).
  47. rewrite subnn//= !binn GRing.expr0//= GRing.mul1r GRing.mulr1n//=.
  48. rewrite EulerFermatPoly //.
  49. rewrite(_ : \sum_(i < n'.+1) 'X^(n - (1 + i)) * a%:P^+ (1 + i) *+ 'C(n, 1 + i) = 0%:P) //=; first by rewrite GRing.add0r.
  50. rewrite(_ : \sum_(i < n'.+1) 'X^(n - (1 + i)) * a%:P^+ (1 + i) *+ 'C(n, 1 + i) = \sum_(i < n'.+1) 0%:P); first by apply/big1.
  51. Search "big".
  52. rewrite(_ : \sum_(i < n'.+1) 'X^(n - (1 + i)) * a%:P ^+ (1 + i) *+ 'C(n, 1 + i) = \sum_(0 <= i < n'.+1) 'X^(n - (1 + i)) * a%:P ^+ (1 + i) *+ 'C(n, 1 + i)).
  53. rewrite(_ : \sum_(i < n'.+1) 0%:P = \sum_(0 <= i < n'.+1) 0%:P).
  54. Search "big" "eq".
  55. apply/eq_big_nat.
  56. move=> i range.
  57. rewrite(_ : 1 + i = i.+1)%N.
  58. have range_Si : (1 <= i.+1 < n)%N; first by rewrite /n; exact: range.
  59. have S_i_dvd_n : (n %| 'C(n, i.+1))%N. by apply/n_dvd_coef.
  60. move: (S_i_dvd_n).
  61. Check dvdnP.
  62. move/dvdnP => Hip_A.
  63. destruct Hip_A.
  64. rewrite H.
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement