Database
BASIC ALGEBRAIC STRUCTURES
Rings
Local rings
clring
Next ⟩
df-lring
Metamath Proof Explorer
Unicode
Structured
Syntax definition
clring
Description:
Extend class notation with class of all local rings.
Ref
Expression
Assertion
clring
class LRing