ccm2 - Mathbox for Jeff Madsen

	Mathbox for Jeff Madsen		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ccm2		Structured version Visualization version GIF version

Syntax Definition ccm2 36074

Description: Extend class notation with a class that adds commutativity to various flavors of rings.

**Assertion**
Ref	Expression
ccm2	class Com2

See definition df-com2 36075 for more information.

Colors of variables: wff setvar class