finrank_bot_le_finrank_of_isScalarTower

English

Under a scalar tower R → S → M with finite M, finrank_S M ≤ finrank_R M.

Русский

При скалярной башне R → S → M с конечным M, выполняется finrank_S M ≤ finrank_R M.

LaTeX

$$$\\operatorname{finrank} S M \\le \\operatorname{finrank} R M$$$

Lean4

/-- Also see `Module.finrank_bot_le_finrank_of_isScalarTower_of_free`
for a version with different typeclass constraints. -/
theorem finrank_bot_le_finrank_of_isScalarTower (S T : Type*) [Semiring S] [Semiring T] [Module R T] [Module S T]
    [Module R S] [IsScalarTower R S T] [IsScalarTower S T T] [FaithfulSMul S T] [Module.Finite R T] :
    finrank R S ≤ finrank R T :=
  finrank_le_finrank_of_rank_le_rank (lift_rank_bot_le_lift_rank_of_isScalarTower R S T) (Module.rank_lt_aleph0 _ _)

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