lie_of_of_ne — Mathlib

English

The bracket on the direct sum restricted to components i and j is zero when i ≠ j, and equals the component bracket otherwise.

Русский

Скобка на прямой сумме между компонентами i и j равна нулю, если i ≠ j, иначе равна скобке внутри компонента i.

LaTeX

$$For i ≠ j, [of L_i x, of L_j y] = 0; for i=j, [of L_i x, of L_i y] = of L_i [x,y].$$

Lean4

theorem lie_of_of_ne [DecidableEq ι] {i j : ι} (hij : i ≠ j) (x : L i) (y : L j) : ⁅of L i x, of L j y⁆ = 0 :=
  by
  ext k
  rw [bracket_apply]
  obtain rfl | hik := Decidable.eq_or_ne k i
  · rw [of_eq_of_ne _ _ _ hij, lie_zero, zero_apply]
  · rw [of_eq_of_ne _ _ _ hik, zero_lie, zero_apply]

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