termℚ_[_] — Mathlib

English

The p-adic numbers form a field under the induced operations.

Русский

P-адиковыe числа образуют поле с заданными операциями.

LaTeX

$$\mathbb{Q}_{(p)} \text{ is a field}$$

Lean4

/-- notation for p-padic rationals -/
@[term_parser 1000]
public meta def «termℚ_[_]» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `«termℚ_[_]» 1024
    (ParserDescr.binary✝ `andthen (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "ℚ_[") (ParserDescr.cat✝ `term 0))
      (ParserDescr.symbol✝ "]"))

Похожие утверждения