rank_bot_le_rank_of_isScalarTower

English

If T carries compatible scalar towers with R and R′, then the rank of R relative to R' does not exceed the rank of T.

Русский

Если T совместим с башнями скаляров R и R', то ранг R относительно R' не превосходит ранг T.

LaTeX

$$$\operatorname{Module.rank} R R' \le \operatorname{Module.rank} R T$$$

Lean4

theorem rank_bot_le_rank_of_isScalarTower (T : Type u') [Module R R'] [NonAssocSemiring T] [Module R T] [Module R' T]
    [IsScalarTower R' T T] [FaithfulSMul R' T] [IsScalarTower R R' T] : Module.rank R R' ≤ Module.rank R T := by
  simpa using Module.lift_rank_bot_le_lift_rank_of_isScalarTower R R' T

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