rootSpan_eq_top_iff — Mathlib

English

The root span equals the top submodule if and only if the coroot span does.

Русский

Корневой Span равен топ-части тогда и только тогда, когда и коройт Span равно топу.

LaTeX

$$P.rootSpan R = ⊤ \\Leftrightarrow P.corootSpan R = ⊤$$

Lean4

theorem rootSpan_eq_top_iff : P.rootSpan R = ⊤ ↔ P.corootSpan R = ⊤ :=
  by
  have : IsReflexive R M := .of_isPerfPair P.toLinearMap
  have : IsReflexive R N := .of_isPerfPair P.flip.toLinearMap
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ <;> apply Submodule.eq_top_of_finrank_eq
  · rw [P.finrank_corootSpan_eq', h, finrank_top, P.toPerfPair.finrank_eq, Subspace.dual_finrank_eq]
  · rw [← P.finrank_corootSpan_eq', h, finrank_top, P.toPerfPair.finrank_eq, Subspace.dual_finrank_eq]

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