finrank_top_le_finrank_of_isScalarTower

English

Let R, S, T form a scalar tower with appropriate finite conditions. Then finrank R S ≤ finrank R T.

Русский

Пусть R, S, T образуют скалярную башню с подходящими условиями конечности. Тогда finrank R S ≤ finrank R T.

LaTeX

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

Lean4

/-- Also see `Module.finrank_top_le_finrank_of_isScalarTower_of_free`
for a version with different typeclass constraints. -/
theorem finrank_top_le_finrank_of_isScalarTower [Module.Finite R M] [Semiring S] [Module S M] [Module R S]
    [IsScalarTower R S S] [FaithfulSMul R S] [IsScalarTower R S M] : finrank S M ≤ finrank R M :=
  by
  rw [finrank, finrank, Cardinal.toNat_le_iff_le_of_lt_aleph0]
  · exact rank_top_le_rank_of_isScalarTower R S M
  · exact lt_of_le_of_lt (rank_top_le_rank_of_isScalarTower R S M) (Module.rank_lt_aleph0 R M)
  · exact Module.rank_lt_aleph0 _ _

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