proposition: Lemma projected_ring: Ring B.
proof: Proof. split. now apply (groups.projected_ab_group f). now apply (groups.projected_com_monoid f mult_correct one_correct). repeat intro; apply (injective f). rewrite plus_correct, !mult_correct, plus_correct. now rewrite distribute_l. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra