proposition: Fact inZpm_is_multiplicative : multiplicative (inZp : 'Z_n -> 'F_p).
proof: Proof. have p_gt1 : 1 < p by apply: prime_gt1. split=> [x y| //]; apply/val_eqP/eqP => /=. set x' := nat_of_ord _; set y' := nat_of_ord _. by rewrite !Zp_cast /= ?pdiv_id // modnMm modn_dvdm. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound