implementations.nonzero_field_elements

Require Import
  Ring
  abstract_algebra
  theory.fields.

Section contents.
Context `{Field F}.
Add Ring F : (rings.stdlib_ring_theory F).

Global Program Instance NonZero_1: RingOne (F ) := (1:F).

Global Program Instance NonZero_mult: RingMult (F ) := λ x y, (`x * `y : F).

Ltac unfold_equiv := repeat intro; unfold equiv, sig_equiv in *; simpl in *.

Instance: Proper ((=) ==> (=) ==> (=)) NonZero_mult.

Global Instance: CommutativeMonoid (F ).

Definition NonZero_inject (x : F ) : F := `x.

Global Instance: SemiGroup_Morphism NonZero_inject (Bop:=(.*.)).

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

Lemma mult_inv_distr `{ z, PropHolds (z 0) LeftCancellation (.*.) z} (x y : F ) :
  // (x * y) = // x * // y.
End contents.