# Untitled

a guest
Nov 29th, 2019
199
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
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//=.
18. assert (n0.+1 >= 2)%N; first by exact: prime_gt1.
19. by rewrite ltnSS.
21. *)
22. Check [idomainType of 'F_n].
23. Lemma EulerFermatPoly : forall (a : 'F_n), prime n -> (polyC a)^+n = polyC a.
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.