finrank_corootSpan_eq' — Mathlib

English

Equality of finrank between corootSpan and rootSpan holds when R is a domain and P is anisotropic.

Русский

Эквивалентность размерностей между corootSpan и rootSpan при доменной базе и анизотропности P.

LaTeX

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

Lean4

/-- Equality of `finrank`s when the base is a domain. -/
theorem finrank_corootSpan_eq' : finrank R (P.corootSpan R) = finrank R (P.rootSpan R) :=
  le_antisymm P.finrank_corootSpan_le' P.flip.finrank_corootSpan_le'

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