fact: Definition rng_homo_mult : f (x * y) = f x * f y := preserves_mult x y.
imports: WildCat Spaces.Nat.Core Classes.interfaces.abstract_algebra Algebra.AbGroups Classes.theory.rings Modalities.ReflectiveSubuniverse