mlieBracket_zero_left — Mathlib

English

The Lie bracket of the zero left argument with any vector field is identically zero.

Русский

Скобка Ли нуля слева с любым векторным полем тождественно равна нулю.

LaTeX

$$$\mathrm{mlieBracket}(I,0,W) = 0$$$

Lean4

/-- We have `[0, W] = 0` for all vector fields `W`: this depends on the junk value 0
if `W` is not differentiable. -/
@[simp]
theorem mlieBracket_zero_left : mlieBracket I 0 W = 0 := by simp [← mlieBracketWithin_univ]

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