Metamath Proof Explorer


Syntax definition cmu

Description: Extend class notation with the Möbius function.

Ref Expression
Assertion cmu class μ