Lean4
/-- We introduce the notations `ordProj[p] n` for the largest power of the prime `p` that
divides `n` and `ordCompl[p] n` for the complementary part. The `ord` naming comes from
the $p$-adic order/valuation of a number, and `proj` and `compl` are for the projection and
complementary projection. The term `n.factorization p` is the $p$-adic order itself.
For example, `ordProj[2] n` is the even part of `n` and `ordCompl[2] n` is the odd part. -/
@[term_parser 1000]
public meta def «termOrdProj[_]_» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Nat.«termOrdProj[_]_» 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "ordProj[") (ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ "] "))
(ParserDescr.cat✝ `term 1023))
