span_eq_top — Mathlib

English

If the root system is irreducible, the span of longRoot P and shortRoot P equals the whole space.

Русский

Если система корней ирредуцируема, тогда линейная оболочка длинного корня и короткого корня покрывает всё пространство.

LaTeX

$$span R {longRoot P, shortRoot P} = ⊤$$

Lean4

@[simp]
theorem span_eq_top : span R {longRoot P, shortRoot P} = ⊤ :=
  by
  have := P.span_root_image_eq_top_of_forall_orthogonal {long P, short P} (by simp)
  rw [show P.root '' {long P, short P} = {longRoot P, shortRoot P} by aesop] at this
  refine this fun k hk ij hij ↦ ?_
  replace hk : P.root k ∉ allRoots P := fun contra ↦ hk <| span_subset_span ℤ _ _ <| mem_span_of_mem_allRoots P contra
  have aux := isOrthogonal_short_and_long P hk
  rcases hij with rfl | rfl <;> tauto

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