fact: Definition Cmult (z z' : Ctype) : Ctype := Build_Ctype (sgroup_law R (ring_mult (real z) (real z')) (group_inverse R (ring_mult (imag z) (imag z')))) (sgroup_law R (ring_mult (real z) (imag z')) (ring_mult (imag z) (real z'))).
imports: Cfield_facts