English
There is an algebra structure on the stalk of smooth maps at a point given by evaluation, making evaluation at x an algebra morphism.
Русский
На локале гладких функций в точке задаётся алгебраическая структура через эвалюацию, превращающая эвалюацию в алгебра-морфизм.
LaTeX
$$$$ \text{evalAlgebra}_x: C^∞⟮I,M; 𝕜⟯⟨x⟩ \to 𝕜 \text{ is an algebra morphism}. $$$$
Lean4
/-- `n`-times continuously differentiable diffeomorphism between `E` and `E'`. -/
@[scoped term_parser 1000]
public meta def «term_≃ₘ^_[_]_» : Lean.TrailingParserDescr✝ :=
ParserDescr.trailingNode✝ `Manifold.«term_≃ₘ^_[_]_» 1022 0
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " ≃ₘ^") (ParserDescr.cat✝ `term 1000))
(ParserDescr.symbol✝ "["))
(ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ "] "))
(ParserDescr.cat✝ `term 0))
