mulInvariantVectorField_eq_mpullback

English

There is an equality showing mulInvariantVectorField equals a pullback expression with g⁻¹• and V.

Русский

Существует равенство, выражающее mulInvariantVectorField через вытягивание (mpullback) через g⁻¹.

LaTeX

$$$mulInvariantVectorField (V 1) g = mpullback I I (g^{-1} * \\cdot) V g$$$

Lean4

@[to_additive]
theorem mulInvariantVectorField_eq_mpullback (g : G) (V : Π (g : G), TangentSpace I g) :
    mulInvariantVectorField (V 1) g = mpullback I I (g⁻¹ * ·) V g :=
  by
  have A : 1 = g⁻¹ * g := by simp
  simp only [mulInvariantVectorField, mpullback, inverse_mfderiv_mul_left]
  congr
  simp

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