theory.fields

Require Import
  Ring abstract_algebra strong_setoids.
Require Export
  theory.rings.

Section field_properties.
Context `{Field F}.

Add Ring F : (stdlib_ring_theory F).

Lemma mult_inverse_alt (x : F) Px : x // xPx = 1.

Lemma mult_inv_proper_alt x y Px Py : x = y // xPx = // yPy.

Lemma mult_inv_irrelevant x Px1 Px2 : // xPx1 = // xPx2.

Lemma apart_0_proper {x y} : x 0 x = y y 0.

Global Instance: StrongInjective (-).

Global Instance: StrongInjective (//).

Global Instance: z, StrongLeftCancellation (+) z.

Global Instance: z, StrongRightCancellation (+) z.

Global Instance: z, PropHolds (z 0) StrongLeftCancellation (.*.) z.

Global Instance: z, PropHolds (z 0) StrongRightCancellation (.*.) z.

Lemma mult_apart_zero_l x y : x * y 0 x 0.

Lemma mult_apart_zero_r x y : x * y 0 y 0.

Instance mult_apart_zero x y :
  PropHolds (x 0) PropHolds (y 0) PropHolds (x * y 0).

Instance: NoZeroDivisors F.

Global Instance: IntegralDomain F.

Global Instance apart_0_sig_apart_0: (x : F ), PropHolds (`x 0).

Instance mult_inv_apart_zero x : PropHolds (// x 0).

Lemma field_div_0_l x y : x = 0 x // y = 0.

Lemma field_div_diag x y : x = `y x // y = 1.

Lemma equal_quotients (a c: F) b d : a * `d = c * `b a // b = c // d.

Lemma mult_inv_distr_alt (x y : F) Px Py Pxy :
  // (x * y)↾Pxy = // xPx * // yPy.
End field_properties.

Hint Extern 8 (PropHolds (// _ 0)) => eapply @mult_inv_apart_zero : typeclass_instances.
Hint Extern 8 (PropHolds (_ * _ 0)) => eapply @mult_apart_zero : typeclass_instances.

Section morphisms.
  Context `{Field F1} `{Field F2} `{!StrongSemiRing_Morphism (f : F1 F2)}.

  Add Ring F1 : (stdlib_ring_theory F1).

  Lemma strong_injective_preserves_0 : ( x, x 0 f x 0) StrongInjective f.

  Global Instance: StrongInjective f.

  Lemma preserves_mult_inv x Px Pfx : f (// xPx) = // (f x)↾Pfx.
End morphisms.