instIsScalarTowerSomeENatTop — Mathlib

English

The space of derivations at a point x on the algebra C^∞⟮I, M; 𝕜⟯⟨x⟩ 𝕜 is the derivation module Derivation 𝕜( C^∞⟮I, M; 𝕜⟯⟨x⟩ 𝕜) with base field 𝕜.

Русский

Пространство дериваторов в точке x над алгеброй C^∞⟮I, M; 𝕜⟯⟨x⟩ 𝕜 образует модуль дериваций над 𝕜.

LaTeX

$$$$ \text{PointDerivation}(x) := \ Derivation_{\mathbb{K}}(C^∞\langle I,M;\mathbb{K}\rangle\langle x\rangle , \mathbb{K}). $$$$

Lean4

instance (x : M) : IsScalarTower 𝕜 C^∞⟮I, M; 𝕜⟯⟨x⟩ 𝕜 where
  smul_assoc k f
    h := by rw [smul_def, smul_def, ContMDiffMap.coe_smul, Pi.smul_apply, smul_eq_mul, smul_eq_mul, mul_assoc]

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