finrank_ulift — Mathlib

English

For any module M over R, the finitary rank (finite dimension) is preserved under ULift: finrank_R(ULift M) = finrank_R M.

Русский

Для модуля M над R сохраняется конечная размерность при ULift: finrank_R(ULift M) = finrank_R M.

LaTeX

$$$\operatorname{finrank}_R(\mathrm{ULift}\,M) = \operatorname{finrank}_R M$$$

Lean4

@[simp]
theorem finrank_ulift : finrank R (ULift M) = finrank R M := by simp_rw [finrank, rank_ulift, toNat_lift]

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