rank_add_rank_le_rank_prod — Mathlib

English

Let M and M1 be modules over a nontrivial ring R. Then rank_R(M) + rank_R(M1) ≤ rank_R(M × M1).

Русский

Пусть M и M1 — модули над не тривиальным кольцом R. Тогда ранк R(M) + ранк R(M1) ≤ ранк R(M × M1).

LaTeX

$$$\operatorname{rank}_R M + \operatorname{rank}_R M_1 \leq \operatorname{rank}_R (M \times M_1)$$$

Lean4

theorem rank_add_rank_le_rank_prod [Nontrivial R] : Module.rank R M + Module.rank R M₁ ≤ Module.rank R (M × M₁) :=
  by
  conv_lhs => simp only [Module.rank_def]
  rw [Cardinal.ciSup_add_ciSup _ (bddAbove_range _) _ (bddAbove_range _)]
  exact ciSup_le fun ⟨s, hs⟩ ↦ ciSup_le fun ⟨t, ht⟩ ↦ (linearIndependent_inl_union_inr' hs ht).cardinal_le_rank

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