rootForm_pos_of_ne_zero — Mathlib

English

Equivalently, rootSpan is top iff corootSpan is top (anisotropic setting).

Русский

Эквивалентно: rootSpan равен верхнему подпростр., если и только если corootSpan равен верхнему подпростр., в анизотропном случае.

LaTeX

$$P.rootSpan R = ⊤ ↔ P.corootSpan R = ⊤$$

Lean4

theorem rootForm_pos_of_ne_zero {x : M} (hx : x ∈ P.rootSpan R) (h : x ≠ 0) : 0 < P.RootForm x x :=
  by
  apply (P.zero_le_rootForm x).lt_of_ne
  contrapose! h
  exact P.eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero hx h.symm

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