posRootForm_posForm_pos_of_ne_zero

English

If x is a nonzero element of the root span, there exists an index i such that the coroot in i has nonzero action on x.

Русский

Пусть x не ноль в корневом пространстве; существует i такой, что корот в i действует на x ненулево.

LaTeX

$$$\exists i, P.coroot'In S i (x) \neq 0$ for some x ∈ P.rootSpan S, x ≠ 0$$

Lean4

theorem posRootForm_posForm_pos_of_ne_zero {x : P.rootSpan S} (hx : x ≠ 0) : 0 < (P.posRootForm S).posForm x x :=
  by
  rw [posRootForm_posForm_apply_apply]
  have := P.isAnisotropic_of_isValuedIn S
  have : ∃ i ∈ Finset.univ, 0 < (P.coroot'In S i) x * (P.coroot'In S i) x :=
    by
    obtain ⟨i, hi⟩ := P.exists_coroot_ne S hx
    use i
    exact ⟨Finset.mem_univ i, mul_self_pos.mpr hi⟩
  exact Finset.sum_pos' (fun i a ↦ mul_self_nonneg ((P.coroot'In S i) x)) this

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