fact: Definition issig_CRingHomomorphism (A B : CRing) : _ <~> CRingHomomorphism A B := ltac:(issig).
imports: WildCat Spaces.Nat.Core Classes.interfaces.abstract_algebra Algebra.AbGroups Classes.theory.rings Modalities.ReflectiveSubuniverse