1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
17 include "nat/orders.ma".
20 let rec gpow (G : abelian_group) (x : G) (n : nat) on n : G ≝
21 match n with [ O ⇒ 0 | S m ⇒ x + gpow ? x m].
23 interpretation "additive abelian group pow" 'times n x =
24 (cic:/matita/divisible_group/gpow.con _ x n).
26 record dgroup : Type ≝ {
27 dg_carr:> abelian_group;
28 dg_prop: ∀x:dg_carr.∀n:nat.∃y.S n * y ≈ x
31 lemma divide: ∀G:dgroup.G → nat → G.
32 intros (G x n); cases (dg_prop G x n); apply w;
35 interpretation "divisible group divide" 'divide x n =
36 (cic:/matita/divisible_group/divide.con _ x n).
39 ∀G:dgroup.∀x:G.∀n. S n * (x / n) ≈ x.
40 intro G; cases G; unfold divide; intros (x n); simplify;
41 cases (f x n); simplify; exact H;
44 lemma feq_mul: ∀G:dgroup.∀x,y:G.∀n.x≈y → n * x ≈ n * y.
45 intros (G x y n H); elim n; [apply eq_reflexive]
46 simplify; apply (Eq≈ (x + (n1 * y)) H1);
47 apply (Eq≈ (y+n1*y) H (eq_reflexive ??));
50 lemma div1: ∀G:dgroup.∀x:G.x/O ≈ x.
51 intro G; cases G; unfold divide; intros; simplify;
52 cases (f x O); simplify; simplify in H; intro; apply H;
53 apply (Ap≪ ? (plus_comm ???));
54 apply (Ap≪ w (zero_neutral ??)); assumption;
57 lemma apmul_ap: ∀G:dgroup.∀x,y:G.∀n.S n * x # S n * y → x # y.
58 intros 4 (G x y n); elim n; [2:
60 cases (applus ????? a); [assumption]
62 apply (plus_cancr_ap ??? 0); assumption;
65 lemma plusmul: ∀G:dgroup.∀x,y:G.∀n.n * (x+y) ≈ n * x + n * y.
66 intros (G x y n); elim n; [
67 simplify; apply (Eq≈ 0 ? (zero_neutral ? 0)); apply eq_reflexive]
68 simplify; apply eq_sym; apply (Eq≈ (x+y+(n1*x+n1*y))); [
69 apply (Eq≈ (x+(n1*x+(y+(n1*y))))); [
70 apply eq_sym; apply plus_assoc;]
71 apply (Eq≈ (x+((n1*x+y+(n1*y))))); [
72 apply feq_plusl; apply plus_assoc;]
73 apply (Eq≈ (x+(y+n1*x+n1*y))); [
74 apply feq_plusl; apply feq_plusr; apply plus_comm;]
75 apply (Eq≈ (x+(y+(n1*x+n1*y)))); [
76 apply feq_plusl; apply eq_sym; apply plus_assoc;]
78 apply feq_plusl; apply eq_sym; assumption;
81 lemma mulzero: ∀G:dgroup.∀n.n*0 ≈ 0. [2: apply dg_carr; apply G]
82 intros; elim n; [simplify; apply eq_reflexive]
83 simplify; apply (Eq≈ ? (zero_neutral ??)); assumption;
86 let rec gpowS (G : abelian_group) (x : G) (n : nat) on n : G ≝
87 match n with [ O ⇒ x | S m ⇒ gpowS ? x m + x].
89 lemma gpowS_gpow: ∀G:dgroup.∀e:G.∀n. S n * e ≈ gpowS ? e n.
90 intros (G e n); elim n; simplify; [
91 apply (Eq≈ ? (plus_comm ???));apply zero_neutral]
92 apply (Eq≈ ?? (plus_comm ???));
93 apply (Eq≈ (e+S n1*e) ? H); clear H; simplify; apply eq_reflexive;
96 lemma divpow: ∀G:dgroup.∀e:G.∀n. e ≈ gpowS ? (e/n) n.
97 intros (G e n); apply (Eq≈ ?? (gpowS_gpow ?(e/n) n));
98 apply eq_sym; apply divide_divides;