a_algebra_properties: is_algebra ? ? a_mult a_one
}.
-interpretation "Algebra product" 'times a b =
- (cic:/matita/attic/integration_algebras/a_mult.con _ a b).
+interpretation "Algebra product" 'times a b = (a_mult _ a b).
definition ring_of_algebra ≝
λK.λA:algebra K.