finrank_corootSpan_eq — Mathlib

English

The coroot span and the root span have the same dimension over S for anisotropic P.

Русский

Область коротов и область корней имеют одинаковую размерность над S для анизотропной P.

LaTeX

$$$\operatorname{finrank}_S(\operatorname{corootSpan} S) = \operatorname{finrank}_S(\operatorname{rootSpan} S)$$$

Lean4

theorem finrank_corootSpan_eq [P.IsAnisotropic] : finrank S (P.corootSpan S) = finrank S (P.rootSpan S) :=
  le_antisymm (P.finrank_corootSpan_le S) (P.flip.finrank_corootSpan_le S)

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