ring — Mathlib

English

There is a standard ring C sending scalars into C^n-maps by constant maps: c ↦ x ↦ algebraMap c, which is a ring homomorphism and preserves smoothness.

Русский

Существует кольцо констант C, отображающее скаляры в C^n-отображения константной картой, сохраняющей гладкость.

LaTeX

$$$C: \mathbb{K}\to C^n(I,N;I',R)\text{ is a ring homomorphism given by } c\mapsto x\mapsto (\text{algebraMap }\mathbb{K}R)(c).$$$

Lean4

instance ring {R : Type*} [Ring R] [TopologicalSpace R] [ChartedSpace H' R] [ContMDiffRing I' n R] :
    Ring C^n⟮I, N; I', R⟯ :=
  { ContMDiffMap.semiring, ContMDiffMap.addCommGroup with }

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