proposition: Lemma encode_morphism_only `{AlgebraOps theory A} `{∀ u, Equiv (A u)} `{AlgebraOps theory B} `{∀ u, Equiv (B u)} (f: ∀ u, A u → B u) `{!Ring (A tt)} `{!Ring (B tt)} `{!SemiRing_Morphism (f tt)}: HomoMorphism sig A B f.
proof: Proof. constructor. intros []. apply _. intros []; simpl. apply rings.preserves_plus. apply rings.preserves_mult. apply rings.preserves_0. apply rings.preserves_1. apply rings.preserves_negate. apply encode_algebra_only. apply encode_algebra_only. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics