fact: Definition rng_homo_compose {A B C : CRing} (f : CRingHomomorphism B C) (g : CRingHomomorphism A B) : CRingHomomorphism A C.
imports: WildCat Spaces.Nat.Core Classes.interfaces.abstract_algebra Algebra.AbGroups Classes.theory.rings Modalities.ReflectiveSubuniverse