C — Mathlib · SciLib

English

The scalar smul distributes over composition with another ContMDiff map: (r•g)∘h = r•(g∘h).

Русский

Существуют совместимые действия SMul на ContMDiffMap над 𝕜, образующие 𝕜-модуль.

LaTeX

$$$ (r\cdot g)\circ h = r\cdot (g\circ h) $$$

Lean4

/-- `C^n` constant functions as a `RingHom`. -/
def C : 𝕜 →+* C^n⟮I, N; 𝓘(𝕜, A), A⟯
    where
  toFun := fun c : 𝕜 => ⟨fun _ => (algebraMap 𝕜 A) c, contMDiff_const⟩
  map_one' := by ext; exact (algebraMap 𝕜 A).map_one
  map_mul' c₁ c₂ := by ext; exact (algebraMap 𝕜 A).map_mul _ _
  map_zero' := by ext; exact (algebraMap 𝕜 A).map_zero
  map_add' c₁ c₂ := by ext; exact (algebraMap 𝕜 A).map_add _ _

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