apply_sum_inl_eq_zero_of_mem_span_h

English

The bracket of h(i) and h(j) vanishes; this expresses a commutativity relation in the sl2-triple construction.

Русский

Скобка h(i) и h(j) равна нулю; выражает отношение коммутативности в конструкции тройки sl2.

LaTeX

$$⟪h i, h j⟫ = 0$$

Lean4

theorem apply_sum_inl_eq_zero_of_mem_span_h (i : b.support) (j : b.support ⊕ ι)
    {x : Matrix (b.support ⊕ ι) (b.support ⊕ ι) R} (hx : x ∈ span R (range h)) : x j (Sum.inl i) = 0 := by
  induction hx using span_induction with
  | mem x h => obtain ⟨i, rfl⟩ := h; cases j <;> simp [h]
  | zero => simp
  | add u v _ _ hu hv => simp [hu, hv]
  | smul t u _ hu => simp [hu]

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