fact: Definition Build_CRing' (R : AbGroup) `(Mult R, One R, LeftDistribute R mult (@group_sgop R)) (iscomm : @IsCommutativeMonoid R mult one) : CRing := Build_CRing R (@group_sgop R) _ (@group_unit R) _ (@group_inverse R) (Build_IsRing _ _ _ _).
imports: WildCat Spaces.Nat.Core Classes.interfaces.abstract_algebra Algebra.AbGroups Classes.theory.rings Modalities.ReflectiveSubuniverse