Metamath Proof Explorer


Syntax definition clogb

Description: Extend class notation to include the logarithm generalized to an arbitrary base.

Ref Expression
Assertion clogb class logb