proposition: Lemma mor_from_sr_to_alg `{InVariety theory A} `{InVariety theory B} (f: ∀ u, A u → B u) `{!SemiRing_Morphism (f tt)}: HomoMorphism sig A B f.
proof: Proof. constructor. intros []. apply _. intros []; simpl. apply rings.preserves_plus. apply rings.preserves_mult. change (f tt 0 = 0). apply rings.preserves_0. change (f tt 1 = 1). apply rings.preserves_1. change (Algebra theory A). apply _. change (Algebra theory B). apply _. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics