span_eq_rootSpan_int — Mathlib

English

If i and j belong to the base support with i ≠ j, then the ℤ-span of {P.root i, P.root j} equals the root span over ℤ: span_ℤ{P.root i, P.root j} = P.rootSpan ℤ.

Русский

Если i и j принадлежат базовому дополнению и i ≠ j, тогда ℤ-оболочка {P.root i, P.root j} совпадает с корневым пространством P.rootSpan ℤ.

LaTeX

$$span ℤ\{P.root i, P.root j\} = P.rootSpan ℤ$$

Lean4

theorem span_eq_rootSpan_int {i j : ι} (hi : i ∈ b.support) (hj : j ∈ b.support) (h_ne : i ≠ j) :
    Submodule.span ℤ {P.root i, P.root j} = P.rootSpan ℤ := by
  classical
  have : { i, j } ⊆ b.support := by grind
  rw [← image_pair, ← Finset.coe_pair, Finset.eq_of_subset_of_card_le this (by aesop), b.span_int_root_support]

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