English
The lifted rank times lifted insepDegree equals lifted base insepDegree: lift(rank_F E) · lift(insepDegree_E K) = lift(insepDegree_F K), given IsPurelyInseparable F E.
Русский
При чистой инsep-степени: lift(rank_F E) · lift(insepDegree_E K) = lift(insepDegree_F K).
LaTeX
$$Cardinal.lift(rank F E) · Cardinal.lift(insepDegree E K) = Cardinal.lift(insepDegree F K)$$
Lean4
/-- If `K / E / F` is a field extension tower, such that `E / F` is purely inseparable,
then $[E:F] [K:E]_i = [K:F]_i$.
It is a special case of `Field.lift_insepDegree_mul_lift_insepDegree_of_isAlgebraic`, and is an
intermediate result used to prove it. -/
theorem lift_rank_mul_lift_insepDegree_of_isPurelyInseparable [IsPurelyInseparable F E] :
Cardinal.lift.{w} (Module.rank F E) * Cardinal.lift.{v} (insepDegree E K) = Cardinal.lift.{v} (insepDegree F K) :=
by
have h :=
(separableClosure F K).linearDisjoint_of_isPurelyInseparable_of_isSeparable
E |>.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic_left
rwa [separableClosure.adjoin_eq_of_isAlgebraic] at h
