lie_of — Mathlib

English

If i=j then [of L_i x, of L_i y] equals of L_i [x,y] with the appropriate isomorphism; if i≠j it's 0.

Русский

Если индексы совпадают, скобка внутри компонента равна образу скобки внутри компонента, иначе — ноль.

LaTeX

$$theorem lie_of [DecidableEq ι] {i j : ι} (hij : i ≠ j) (x : L i) (y : L j) : [of L i x, of L j y] = 0.$$

Lean4

@[simp]
theorem lie_of [DecidableEq ι] {i j : ι} (x : L i) (y : L j) :
    ⁅of L i x, of L j y⁆ = if hij : i = j then of L i ⁅x, hij.symm.recOn y⁆ else 0 :=
  by
  obtain rfl | hij := Decidable.eq_or_ne i j
  · simp only [lie_of_same L x y, dif_pos]
  · simp only [lie_of_of_ne L hij x y, hij, dite_false]

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