apply_inr_eq_zero_of_mem_span_range_u

English

The span of the range of h' equals the top Cartan subalgebra inside cartanSubalgebra'(b); this provides a spanning property for the Cartan in the new presentation.

Русский

Область линейной оболочки образа h' равна верхней Картановой подалгебре внутри cartanSubalgebra'(b); это обеспечивает порождение Картановой части в новой презентации.

LaTeX

$$$\operatorname{span}(\operatorname{range} h') = \top$ в cartanSubalgebra'(b)$$

Lean4

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

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