rank_right_mul_adjoin_rank_eq_of_isAlgebraic_left

English

If A and B embed into a common field K via injective homomorphisms and A ⊗F B is a domain, there exists a field K with embeddable images of A and B that are linearly disjoint.

Русский

Если A и B введены в одно поле K посредством инъективных гомоморфизмов и A ⊗F B является областью, существует поле K, куда A и B можно вложить линейно раздельно.

LaTeX

$$$\exists K \;\exists fa fb \; (fa: A \to_K F), (fb: B \to_K F) \text{ с } fa.fieldRange.LinearDisjoint fb.fieldRange$$$

Lean4

theorem rank_right_mul_adjoin_rank_eq_of_isAlgebraic_left (H : A.LinearDisjoint L) [Algebra.IsAlgebraic F A] :
    Module.rank F L * Module.rank (adjoin L (A : Set E)) E = Module.rank A E :=
  H.rank_right_mul_adjoin_rank_eq_of_isAlgebraic (.inl ‹_›)

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