Divisibility. `a ∣ b`

(typed as `\|`

) means that there is some `c`

such that `b = a * c`

.

## Equations

- «term_∣_» = Lean.ParserDescr.trailingNode `term_∣_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∣ ") (Lean.ParserDescr.cat `term 51))