finrank_sup_eq_finrank_left_mul_finrank_of_free

English

In the finite-rank setting under the same freeness hypotheses, the finite rank (dimension) of the join equals the product of the finite rank of A and the finite rank of the adjoint B over A: finrank_R(A ⊔ B) = finrank_R A · finrank_A(adjoin_A(B)).

Русский

В конечном случае ранги (размерности) удовлетворяют аналогичной формуле: finrank_R(A ⊔ B) = finrank_R A · finrank_A(adjoin_A(B)).

LaTeX

$$finrank_sup_eq_finrank_left_mul_finrank_of_free : finrank R ↥(A ⊔ B) = finrank R A * finrank A (Algebra.adjoin A (B : Set S))$$

Lean4

theorem finrank_sup_eq_finrank_left_mul_finrank_of_free :
    finrank R ↥(A ⊔ B) = finrank R A * finrank A (Algebra.adjoin A (B : Set S)) := by
  simpa only [map_mul] using congr(Cardinal.toNat $(rank_sup_eq_rank_left_mul_rank_of_free A B))

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