lift_insepDegree_mul_lift_insepDegree_of_isAlgebraic

English

For any tower F ⊂ E ⊂ K with E/F algebraic, the insepDegree satisfies the tower law: insepDegree F E · insepDegree E K = insepDegree F K.

Русский

Для любой башни F ⊂ E ⊂ K, где E/F алгебраично, insepDegree удовлетворяет закону башни: insepDegree F E · insepDegree E K = insepDegree F K.

LaTeX

$$insepDegree F E · insepDegree E K = insepDegree F K$$

Lean4

/-- If `K / E / F` is a field extension tower, such that `E / F` is algebraic, then their
inseparable degrees satisfy the tower law: $[E:F]_i [K:E]_i = [K:F]_i$. -/
theorem lift_insepDegree_mul_lift_insepDegree_of_isAlgebraic [Algebra.IsAlgebraic F E] :
    Cardinal.lift.{w} (insepDegree F E) * Cardinal.lift.{v} (insepDegree E K) = Cardinal.lift.{v} (insepDegree F K) :=
  by
  have h := lift_rank_mul_lift_insepDegree_of_isPurelyInseparable (separableClosure F E) E K
  rwa [← insepDegree_eq_of_isSeparable F (separableClosure F E) K] at h

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