term_∙_ — Mathlib

English

The span of r • s is contained in the span of s, for any scalar r.

Русский

Замыкание по скаляру r действует так, что span (r • s) ⊆ span s.

LaTeX

$$$$ \operatorname{span} R (r \cdot s) \leq \operatorname{span} R s $$$$

Lean4

@[term_parser 1000]
public meta def «term_∙_» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `Submodule.«term_∙_» 1000 0
    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " ∙ ") (ParserDescr.cat✝ `term 0))

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