term_⋆_ — Mathlib

English

If y is a scalar and there is a compatible SMul class, then y times the convolution equals the convolution with the scalar factor: y·(f ⋆ g) = (y·f) ⋆ g.

Русский

Если дан скаляр y и наличие совместного умножения, то y⋅(f⋆g) = (y⋅f)⋆g.

LaTeX

$$$y\\cdot (f⋆[L,μ]g) = (y\\cdot f)⋆[L,μ]g$$$

Lean4

/-- The convolution of two real-valued functions with respect to volume. -/
@[scoped term_parser 1000]
public meta def «term_⋆_» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `Convolution.«term_⋆_» 67 0
    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " ⋆ ") (ParserDescr.cat✝ `term 66))

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