bracket_def — Mathlib

English

Re-states the bracket definition and its equality with the mlieBracket construction.

Русский

Повторно формулируется определение скобки и её равенство конструкции mlieBracket.

LaTeX

$$$⁅v,w⁆ = mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) (1 : G)$$$

Lean4

@[to_additive]
theorem bracket_def (v w : GroupLieAlgebra I G) :
    ⁅v, w⁆ = mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) (1 : G) :=
  rfl

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