fact: Definition invfraction_fun : fract_field_ring -> fract_field_ring := fun x : fraction_set => match zero_dec (num x) with | left _ => x | right n => Build_fraction (den x) (num x) n end.
imports: Integral_domain_facts Cfield_cat Abelian_group_facts Ring_util