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.