rank_sup_le_of_isAlgebraic — Mathlib

English

If E1 and E2 are finite-dimensional over K, then their join is finite-dimensional over K.

Русский

Если E1 и E2 конечномерны над K, то их объединение также конечномерно над K.

LaTeX

$$∈(FiniteDimensional K E1) ∧ (FiniteDimensional K E2) ⇒ FiniteDimensional K (E1 ⊔ E2)$$

Lean4

/-- If `E1` and `E2` are intermediate fields, and at least one them are algebraic, then the rank of
the compositum of `E1` and `E2` is less than or equal to the product of that of `E1` and `E2`.
Note that this result is also true without algebraic assumption,
but the proof becomes very complicated. -/
theorem rank_sup_le_of_isAlgebraic (halg : Algebra.IsAlgebraic K E1 ∨ Algebra.IsAlgebraic K E2) :
    Module.rank K ↥(E1 ⊔ E2) ≤ Module.rank K E1 * Module.rank K E2 :=
  by
  have := E1.toSubalgebra.rank_sup_le_of_free E2.toSubalgebra
  rwa [← sup_toSubalgebra_of_isAlgebraic E1 E2 halg] at this

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