{R : Ring} (r : R) : GroupHomomorphism R R := @Build_GroupHomomorphism R R (fun s => r * s) (rng_dist_l r).
Require Import WildCat. Require Import Spaces.Nat.Core Spaces.Nat.Arithmetic. Require Import Classes.interfaces.abstract_algebra. Require Import Algebra.Groups.Group Algebra.Groups.Subgroup. Require Import Modalities.ReflectiveSubuniverse.