Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Complexity theory
Digits
cdig
Next ⟩
df-dig
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
cdig
Description:
Extend class notation with the class of the digit extraction operation.
Ref
Expression
Assertion
cdig
class
digit