term_⊗ₖ_ — Mathlib

English

A variant stating the compatibility of kroneckerMap with right reindexing under equivalences.

Русский

Вариант совместимости kroneckerMap с правым переназначением индексов при эквивалентностях.

LaTeX

$$$\kroneckerMap f M (\mathrm{reindex}\ em\ en N) = \mathrm{reindex} ((\mathrm{Equiv.refl _}).prodCongr em) ((\mathrm{Equiv.refl _}).prodCongr en) (\kroneckerMap f M N)$$$

Lean4

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

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