]> matita.cs.unibo.it Git - helm.git/blob - matita/dama/fields.ma
New dependency over acic_procedural.
[helm.git] / matita / dama / fields.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 set "baseuri" "cic:/matita/fields/".
16
17 include "rings.ma".
18
19 record is_field (R:ring) (inv:∀x:R.x ≠ 0 → R) : Prop
20
21  {  (* multiplicative abelian properties *)
22     mult_comm_: symmetric ? (mult R);
23     (* multiplicative group properties *)
24     inv_inverse_: ∀x.∀p: x ≠ 0. inv x p * x = 1
25  }.
26
27 lemma opp_opp: ∀R:ring. ∀x:R. --x=x.
28 intros; 
29 apply (cancellationlaw ? (-x) ? ?); 
30 rewrite > (opp_inverse R x); 
31 rewrite > plus_comm;
32 rewrite > opp_inverse;
33 reflexivity.
34 qed.
35
36 let rec sum (C:Type) (plus:C→C→C) (zero,one:C) (n:nat) on n  ≝
37  match n with
38   [ O ⇒ zero
39   | (S m) ⇒ plus one (sum C plus zero one m)
40   ].
41
42 record field : Type \def
43  { f_ring:> ring;
44    inv: ∀x:f_ring. x ≠ 0 → f_ring;
45    field_properties: is_field f_ring inv
46  }.
47  
48 theorem mult_comm: ∀F:field.symmetric ? (mult F).
49  intro;
50  apply (mult_comm_ ? ? (field_properties F)).
51 qed.
52
53 theorem inv_inverse: ∀F:field.∀x:F.∀p: x ≠ 0. (inv ? x p)*x = 1.
54  intro;
55  apply (inv_inverse_ ? ? (field_properties F)).
56 qed.
57
58 (*CSC: qua funzionava anche mettendo ? al posto della prima F*)
59 definition sum_field ≝
60  λF:field. sum F (plus F) 0 1.