Ringβ βAβ βββ βββ βI\textbf{Ring} \; A \; \otimes \; \oplus \; IRingAββI
RightUnitβ βAβ βββ βU\textbf{RightUnit} \; A \; \otimes \; URightUnitAβU
pred UnitRing(A: set univ, tms,pls: univ->univ->univ, I,U: univ){ Ring[A,tms,pls,I] RightUnit[A,tms,U] }
Last updated 1 year ago