proposition: Lemma Sum0_ring_hom : forall R S (phi : RingHom R S) f n, phi (Sum0 n f) [=] Sum0 n (fun i => phi (f i)).
proof: Proof. intros. induction n; [apply rh_pres_zero|]. simpl; rewrite -> rh_pres_plus, IHn; reflexivity. Qed.
imports: CPoly_Degree CRing_Homomorphisms Qring Zring Qordfield RingClass CRingClass Zlcm Q_can nat_Q_lists RX_deg QX_ZX