proposition: Lemma invert_monoid_morphism: ∀ `{!Inverse f}, Bijective f → Monoid_Morphism f → Monoid_Morphism (f⁻¹).
proof: Proof. intros. pose proof (encode_morphism_and_ops (f:=f)) as P. pose proof (@invert_homomorphism theory _ _ _ _ _ _ _ _ _ _ P) as Q. pose proof (monmor_a (f:=f)). pose proof (monmor_b (f:=f)). apply (@decode_morphism_and_ops _ _ _ _ _ _ _ _ _ Q). Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.misc.workaround_tactics MathClasses.categories.categories