finrank_left_dvd_finrank_sup_of_free

English

Let R,S be commutative rings, A,B subalgebras of S with an R-algebra structure. If A is free as an R-module and the algebra A ⊔ B is free over A, then the (finite) rank of A divides the rank of A ⊔ B, i.e. finrank_R(A) ∣ finrank_R((A ⊔ B)).

Русский

Пусть R,S — коммутативные кольца, A,B — подполья S над R, причём A является свободным модулем над R и A ⊔ B свободно над A. Тогда конечный размер (ранг) пространства A делит ранг пространства A ⊔ B: finrank_R(A) | finrank_R((A ⊔ B)).

LaTeX

$$$\operatorname{finrank}_R A \mid \operatorname{finrank}_R \; \big(\operatorname{Subtype fun x => x \in (A \sqcup B)}\big)$$$

Lean4

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

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