finInsepDegree_mul_finInsepDegree_of_isAlgebraic

English

The natural-number version of the inseparable degree tower law: finInsepDegree F E × finInsepDegree E K = finInsepDegree F K, under algebraicity of E over F.

Русский

Естественный числовой аналог закона башни по инsep-степеням: finInsepDegree F E × finInsepDegree E K = finInsepDegree F K при алгебраичности E над F.

LaTeX

$$finInsepDegree F E · finInsepDegree E K = finInsepDegree F K$$

Lean4

/-- If `K / E / F` is a field extension tower, such that `E / F` is algebraic, then their
inseparable degrees, as natural numbers, satisfy the tower law: $[E:F]_i [K:E]_i = [K:F]_i$. -/
@[stacks 09HK "Part 2, `finInsepDegree` variant"]
theorem finInsepDegree_mul_finInsepDegree_of_isAlgebraic [Algebra.IsAlgebraic F E] :
    finInsepDegree F E * finInsepDegree E K = finInsepDegree F K := by
  simpa only [map_mul, Cardinal.toNat_lift] using
    congr(Cardinal.toNat $(lift_insepDegree_mul_lift_insepDegree_of_isAlgebraic F E K))

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