toFun_eq_coe — Mathlib

English

There is a LinearMapClass instance for LeftInvariantDerivation mapping to ContMDiff maps, respecting 𝕜-linear structure.

Русский

Существует инстанс LinearMapClass для LeftInvariantDerivation, переводящий его в ContMDiff отображения, сохраняющий линейность над 𝕜.

LaTeX

$$Instance: LinearMapClass (LeftInvariantDerivation I G) 𝕜 (ContMDiffMap ...) (ContMDiffMap ...)$$

Lean4

theorem toFun_eq_coe : X.toFun = ⇑X :=
  rfl

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