termC^_⟮_,_;_⟯⟨_⟩ — Mathlib

English

There is a canonical commutative ring structure on pointed C^∞ maps over each fiber.

Русский

Для каждого волокна существует каноническая коммутативная кольцевая структура на указанных C^∞ отображениях.

LaTeX

$$$\text{CommRing } (PointedContMDiffMap 𝕜 I M (WithTop.some instTopENat.top) x)$$$

Lean4

@[inherit_doc PointedContMDiffMap, scoped term_parser 1000]
public meta def «termC^_⟮_,_;_⟯⟨_⟩» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Derivation.«termC^_⟮_,_;_⟯⟨_⟩» 1024
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen
              (ParserDescr.binary✝ `andthen
                (ParserDescr.binary✝ `andthen
                  (ParserDescr.binary✝ `andthen
                    (ParserDescr.binary✝ `andthen
                      (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "C^") (ParserDescr.cat✝ `term 0))
                      (ParserDescr.symbol✝ "⟮"))
                    (ParserDescr.cat✝ `term 0))
                  (ParserDescr.symbol✝ ", "))
                (ParserDescr.cat✝ `term 0))
              (ParserDescr.symbol✝ "; "))
            (ParserDescr.cat✝ `term 0))
          (ParserDescr.symbol✝ "⟯⟨"))
        (ParserDescr.cat✝ `term 0))
      (ParserDescr.symbol✝ "⟩"))

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