English
Under linear disjointness, the product of lifted ranks for L and adjoin(L,A) over E equals the lifted rank of A over E.
Русский
При условии линейной независимости произведение тильдованных рангов L и адъюнкта над E равно тильдованному рангу A над E.
LaTeX
$$$\operatorname{lift}([L:F]) \cdot \operatorname{lift}([\mathrm{adjoin}_L(A) : E]) = \mathrm{rank}_E(A)$$$
Lean4
/-- If `A` is an intermediate field of `E / F`, `L` is an abstract field between `E / F`,
such that they are linearly disjoint over `F`, and one of them is algebraic, then
`[L : F] * [E : L(A)] = [E : A]`. -/
theorem lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic (H : A.LinearDisjoint L)
(halg : Algebra.IsAlgebraic F A ∨ Algebra.IsAlgebraic F L) :
Cardinal.lift.{v} (Module.rank F L) * Cardinal.lift.{w} (Module.rank (adjoin L (A : Set E)) E) =
Cardinal.lift.{w} (Module.rank A E) :=
by
rw [← H.lift_adjoin_rank_eq_lift_rank_right_of_isAlgebraic halg, ← Cardinal.lift_mul, Cardinal.lift_inj]
exact
rank_mul_rank A (extendScalars (show A ≤ (adjoin L (A : Set E)).restrictScalars F from subset_adjoin L (A : Set E)))
E
