term_⊙_ — Mathlib

English

If α is commutative, the Hadamard product is commutative: A ⊙ B = B ⊙ A.

Русский

Если алгебраическая система коммутативна, Hadamard-произведение коммутативно: A ⊙ B = B ⊙ A.

LaTeX

$$$A \odot B = B \odot A$$$

Lean4

@[inherit_doc Matrix.hadamard, scoped term_parser 1000]
public meta def «term_⊙_» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `Matrix.«term_⊙_» 100 100
    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " ⊙ ") (ParserDescr.cat✝ `term 101))

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