proposition: Lemma encode_morphism_and_ops `{Group A} `{Group B} `{!Monoid_Morphism (f: A → B)}: @HomoMorphism sig (λ _, A) (λ _, B) _ _ ( _) ( _) (λ _, f).
proof: Proof. intros. apply encode_morphism_only; assumption. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics categories.categories