GrupaPrzemiennaModulo.v 1.4 KB

1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253
  1. From mathcomp Require Import all_ssreflect.
  2. From mathcomp Require Import ssralg.
  3. Set Implicit Arguments.
  4. Unset Strict Implicit.
  5. Unset Printing Implicit Defensive.
  6. (*
  7. Poniższa sekcja to kopia rozdziału 8.1 z "Math Components Book" (https://math-comp.github.io/mcb/)
  8. Nie mogłem tego znaleźć w bibliotece
  9. *)
  10. Section CalkowiteModulo.
  11. Variable n' : nat.
  12. Notation n := n'.+1.
  13. Implicit Types x y : 'I_n.
  14. Definition inZp i := Ordinal (ltn_pmod i (ltn0Sn n')).
  15. Definition Zp0 : 'I_n := ord0.
  16. Definition Zp1 := inZp 1.
  17. Definition Zp_opp x := inZp (n - x).
  18. Definition Zp_add x y := inZp (x + y).
  19. Definition Zp_mul x y := inZp (x * y).
  20. Ltac odwin := intro x; intros; apply: eqP; rewrite /Zp_add /Zp_mul /inZp /eq_op /=.
  21. Lemma Zp_add0z : left_id Zp0 Zp_add.
  22. Proof.
  23. by odwin; rewrite add0n modn_small.
  24. Qed.
  25. Lemma Zp_mulC : commutative Zp_mul.
  26. Proof.
  27. by odwin; rewrite mulnC.
  28. Qed.
  29. Lemma Zp_addC : commutative Zp_add.
  30. Proof.
  31. by odwin; rewrite addnC.
  32. Qed.
  33. Lemma Zp_addA : associative Zp_add.
  34. Proof.
  35. by odwin; rewrite modnDml modnDmr addnA.
  36. Qed.
  37. Lemma Zp_addNz : left_inverse Zp0 Zp_opp Zp_add.
  38. by odwin; rewrite modnDml subnK; [rewrite modnn | apply: ltnW; rewrite ltn_ord].
  39. Qed.
  40. Definition Zp_zmodMixin := ZmodMixin Zp_addA Zp_addC Zp_add0z Zp_addNz.
  41. Canonical Zp_zmodType := ZmodType 'I_n Zp_zmodMixin.
  42. End CalkowiteModulo.