proposition: Lemma Sum_ring_hom : forall R S (phi : RingHom R S) f i j, phi (Sum i j f) [=] Sum i j (fun i => phi (f i)).
proof: Proof. intros; unfold Sum, Sum1; simpl. rewrite -> rh_pres_minus, rh_pres_plus. rewrite -> Sum0_ring_hom, Sum0_ring_hom; reflexivity. Qed.
imports: CPoly_Degree CRing_Homomorphisms Qring Zring Qordfield RingClass CRingClass Zlcm Q_can nat_Q_lists RX_deg QX_ZX