lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic

English

If K/E/F is a tower with E/F algebraic, then the tower law for separable degrees holds: sepDegree F E · sepDegree E K = sepDegree F K.

Русский

Если K/E/F образуют башню и E/F алгебраично, то тождение для сепарабельных степеней выполняется: sepDegree(F,E) · sepDegree(E,K) = sepDegree(F,K).

LaTeX

$$sepDegree F E · sepDegree E K = sepDegree F K$$

Lean4

/-- If `K / E / F` is a field extension tower, such that `E / F` is algebraic, then their
separable degrees satisfy the tower law: $[E:F]_s [K:E]_s = [K:F]_s$. -/
theorem lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic [Algebra.IsAlgebraic F E] :
    Cardinal.lift.{w} (sepDegree F E) * Cardinal.lift.{v} (sepDegree E K) = Cardinal.lift.{v} (sepDegree F K) :=
  by
  have h := lift_rank_mul_lift_sepDegree_of_isSeparable F (separableClosure F E) K
  rwa [sepDegree_eq_of_isPurelyInseparable (separableClosure F E) E K] at h

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