lieBracketWithin_self

Mathlib.Analysis.Calculus.VectorField

URI: https://scilib.ai/kg/mathlib#VectorField.lieBracketWithin_self

English

lieBracketWithin 𝕜 V V s = 0 for any V; the bracket of a field with itself is zero.

Русский

Скобка внутри поля с самим собой равна нулю.

LaTeX

$$$\operatorname{lieBracketWithin} 𝕜 V V s = 0$$$

Lean4

@[simp]
theorem lieBracketWithin_self : lieBracketWithin 𝕜 V V s = 0 := by ext x; simp [lieBracketWithin]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru