term_D+_ — Mathlib

English

There is a vector-level equivalence between DiophPFun on vectors and Dioph on graphs.

Русский

Существует эквивалентность на уровне векторов между DiophPFun и графами.

LaTeX

$$$$\mathrm{DiophPFun}(f) \iff \mathrm{Dioph}(f.graph)$$$$

Lean4

@[inherit_doc Dioph.add_dioph, scoped term_parser 1000]
public meta def «term_D+_» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `Dioph.«term_D+_» 80 80
    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " D+ ") (ParserDescr.cat✝ `term 81))

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