Metamath Proof Explorer


Syntax definition claz

Description: Extend class notation with the linear adjunctions of a complex number to the ring of integers.

Ref Expression
Assertion claz
class Z[]l