instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall

English

There is an instance declaring the triangularizability of the Lie module associated to cartanSubalgebra'

Русский

Существует инстанс, задающий треугольность модуля Ли, связанного с cartanSubalgebra'.

LaTeX

$$LieModule.IsTriangularizable(cartanSubalgebra'(b), Sum(...))$$

Lean4

instance : LieModule.IsTriangularizable R (cartanSubalgebra' b) (b.support ⊕ ι → R) :=
  by
  refine ⟨fun ⟨⟨x, hx'⟩, hx⟩ ↦ ?_⟩
  obtain ⟨d, rfl⟩ : ∃ d : b.support ⊕ ι → R, Matrix.diagonal d = x :=
    span_range_h_le_range_diagonal <| by simpa using hx
  simp

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