evalAt_mul — Mathlib

English

The bracket operation is well-defined as a LeftInvariantDerivation.

Русский

Скобочная операция определена как левоинвариантный вывод.

LaTeX

$$$ \mathrm{Bracket}(I,G) \text{ yields a LeftInvariantDerivation}(I,G). $$$

Lean4

theorem evalAt_mul : evalAt (g * h) X = 𝒅ₕ (L_apply I g h) (evalAt h X) :=
  by
  ext f
  rw [← left_invariant, hfdifferential_apply, hfdifferential_apply, L_mul, fdifferential_comp, fdifferential_apply]
  simp only [ContMDiffMap.comp_apply, LinearMap.comp_apply]
  rw [fdifferential_apply, ← hfdifferential_apply (smoothLeftMul_one I h), left_invariant]

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