fact: Record ring_algebra_on (A : algebra) : Type := {ring_algebra_assoc : forall x y z : A, Equal (algebra_mult (algebra_mult x y) z) (algebra_mult x (algebra_mult y z)); ring_algebra_unit : A; ring_algebra_unit_l : forall x : A, Equal (algebra_mult ring_algebra_unit x) x; ring_algebra_unit_r : forall x : A, Equal (algebra_mult x ring_algebra_unit) x}.
imports: Hom_module