lift_rank_add_lift_rank_le_rank_prod

English

For nontrivial R, lift(rank_R M) + lift(rank_R M') ≤ rank_R(M × M').

Русский

Пусть R ненулевое, тогда lift(ранг_R M) + lift(ранг_R M') ≤ ранг_R(M × M').

LaTeX

$$$\operatorname{lift}\bigl(\operatorname{rank}_R M\bigr) + \operatorname{lift}\bigl(\operatorname{rank}_R M'\bigr) \leq \operatorname{rank}_R (M \times M')$$$

Lean4

theorem lift_rank_add_lift_rank_le_rank_prod [Nontrivial R] :
    lift.{v'} (Module.rank R M) + lift.{v} (Module.rank R M') ≤ Module.rank R (M × M') :=
  by
  rw [← rank_ulift, ← rank_ulift]
  exact (rank_add_rank_le_rank_prod R _).trans_eq (ULift.moduleEquiv.prodCongr ULift.moduleEquiv).rank_eq

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