term_⍟_ — Mathlib

English

Equality expressing that LSeries.convolution equals the convolution expressed via arithmetic function multiplication.

Русский

Эквивалентность выражений LSeries.convolution через конволюцию и умножение арифметических функций.

LaTeX

$$$f \\star g = f \\cdot g\\quad\\text{(as arithmetic functions).}$$$

Lean4

@[inherit_doc LSeries.convolution, scoped term_parser 1000]
public meta def «term_⍟_» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `LSeries.notation.«term_⍟_» 70 70
    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " ⍟ ") (ParserDescr.cat✝ `term 71))

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