+ (* ring properties *)
+ mult_plus_distr_left: distributive ? mult plus;
+ mult_plus_distr_right: distributive_right C mult plus
+ }.
+
+record ring : Type \def
+ { r_carrier:> Type;
+ r_plus: r_carrier → r_carrier → r_carrier;
+ r_mult: r_carrier → r_carrier → r_carrier;
+ r_zero: r_carrier;
+ r_opp: r_carrier → r_carrier;
+ r_ring_properties:> is_ring ? r_plus r_mult r_zero r_opp
+ }.
+
+notation "0" with precedence 89
+for @{ 'zero }.
+
+interpretation "Ring zero" 'zero =
+ (cic:/matita/integration_algebras/r_zero.con _).
+
+interpretation "Ring plus" 'plus a b =
+ (cic:/matita/integration_algebras/r_plus.con _ a b).
+
+interpretation "Ring mult" 'times a b =
+ (cic:/matita/integration_algebras/r_mult.con _ a b).
+
+interpretation "Ring opp" 'uminus a =
+ (cic:/matita/integration_algebras/r_opp.con _ a).
+
+lemma eq_mult_zero_x_zero: ∀R:ring.∀x:R.0*x=0.
+ intros;
+ generalize in match (zero_neutral ? ? ? ? R 0); intro;
+ generalize in match (eq_f ? ? (λy.y*x) ? ? H); intro; clear H;
+ rewrite > (mult_plus_distr_right ? ? ? ? ? R) in H1;
+ generalize in match (eq_f ? ? (λy.-(0*x)+y) ? ? H1); intro; clear H1;
+ rewrite < (plus_assoc ? ? ? ? R) in H;
+ rewrite > (opp_inverse ? ? ? ? R) in H;
+ rewrite > (zero_neutral ? ? ? ? R) in H;
+ assumption.
+qed.
+
+record is_field (C:Type) (plus:C→C→C) (mult:C→C→C) (zero,one:C) (opp:C→C)
+ (inv:∀x:C.x ≠ zero →C) : Prop
+≝
+ { (* ring properties *)
+ ring_properties: is_ring ? plus mult zero opp;
+ (* multiplicative abelian properties *)