tacticGhost_fun_tac_,_ — Mathlib

English

For the empty matrix representation, the coefficient at index j equals the j-th coordinate of the represented function.

Русский

Для пустой матричной репрезентации коэффициент с индексом j равен j-ой координате соответствующей функции.

LaTeX

$$$\\operatorname{coeff}(\\mathrm{Matrix.vecEmpty}(i), j) = (\\mathrm{Matrix.vecEmpty}(i))(j)$$$

Lean4

/-- An auxiliary tactic for proving that `ghostFun` respects the ring operations. -/
@[tactic_parser 1000]
public meta def «tacticGhost_fun_tac_,_» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `WittVector.«tacticGhost_fun_tac_,_» 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "ghost_fun_tac " false✝)
          (ParserDescr.cat✝ `term 0))
        (ParserDescr.symbol✝ ", "))
      (ParserDescr.cat✝ `term 0))

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