finrank_rootSpan_map_polarization_eq_finrank_corootSpan

English

In an anisotropic reduced irreducible root system, the finiteness dimension of corootSpan equals that of rootSpan.

Русский

При анизотропной редуцированной нерелизируемой корневой системе размерность коротового пространства равна размерности корневого пространства.

LaTeX

$$$\operatorname{finrank}_R(\operatorname{corootSpan} R) = \operatorname{finrank}_R(\operatorname{rootSpan} R)$$$

Lean4

@[simp]
theorem finrank_rootSpan_map_polarization_eq_finrank_corootSpan :
    finrank R ((P.rootSpan R).map P.Polarization) = finrank R (P.corootSpan R) := by
  rw [← P.finrank_range_polarization_eq_finrank_span_coroot R, range_polarizationIn]

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