finrank_right_dvd_finrank_sup_of_free

English

Let R,S,A,B be as above with the given freeness hypotheses. Then finrank_R B divides finrank_R(A ⊔ B).

Русский

Пусть R,S,A,B — как выше, с условиями свободы. Тогда finrank_R(B) делит finrank_R(A ⊔ B).

LaTeX

$$$\operatorname{finrank}_R B \mid \operatorname{finrank}_R \big( A \sqcup B \big)$$$

Lean4

theorem finrank_right_dvd_finrank_sup_of_free : finrank R B ∣ finrank R ↥(A ⊔ B) :=
  ⟨_, finrank_sup_eq_finrank_right_mul_finrank_of_free A B⟩

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