finrank_sup_eq_finrank_right_mul_finrank_of_free

English

Let R,S,A,B be as above with B and the adjoined algebra free over B. Then the finrank of the join equals the product of finrank over A and the finrank of the adjoined over A, i.e., finrank_R(A ⊔ B) = finrank_R(A) · finrank_A(Algebra.adjoin_A(B:Set S)).

Русский

Пусть R,S,A,B — как выше; если B и адъойнт образуются свободно над A, то finrank_R(A ⊔ B) = finrank_R(A) · finrank_A(Algebra.adjoin_A(B:Set S)).

LaTeX

$$$\operatorname{finrank}_R (A \sqcup B) = \operatorname{finrank}_R A \cdot \operatorname{finrank}_{A}(\operatorname{Algebra.adjoin} (A) (B : \mathrm{Set} S))$$$

Lean4

theorem finrank_sup_eq_finrank_right_mul_finrank_of_free :
    finrank R ↥(A ⊔ B) = finrank R B * finrank B (Algebra.adjoin B (A : Set S)) := by
  rw [sup_comm, finrank_sup_eq_finrank_left_mul_finrank_of_free]

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