English
If M is finite over S and there is a scalar tower R → S → S and other compatibility conditions, then finrank_S M ≤ finrank_R M.
Русский
При наличии башни скаляров R → S и прочих условий, если M конечно над S, то finrank_S M ≤ finrank_R M.
LaTeX
$$$$ \\text{finrank}_S(M) \\le \\text{finrank}_R(M) $$$$
Lean4
/-- Also see `Module.finrank_top_le_finrank_of_isScalarTower`
for a version with different typeclass constraints. -/
theorem finrank_top_le_finrank_of_isScalarTower_of_free [Semiring S] [StrongRankCondition S] [Module S M] [Module R S]
[FaithfulSMul R S] [Module.Finite R S] [IsScalarTower R S S] [IsScalarTower R S M] [Module.Free S M] :
finrank S M ≤ finrank R M := by
by_cases H : Module.Finite S M
· have := Module.Finite.trans (R := R) S M
exact finrank_top_le_finrank_of_isScalarTower R S M
· rw [finrank, Cardinal.toNat_eq_zero.mpr (.inr _)]
· exact zero_le _
· rwa [← not_lt, Module.rank_lt_aleph0_iff]
