Database
ELEMENTARY NUMBER THEORY
Elementary properties of divisibility
The divides relation
cdvds
Next ⟩
df-dvds
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
cdvds
Description:
Extend the definition of a class to include the divides relation. See
df-dvds
.
Ref
Expression
Assertion
cdvds
class
∥