English
For a tower F ⊆ E ⊆ K with E/K algebraic, the separable degrees multiply: [E:F]_s · [K:E]_s = [K:F]_s.
Русский
Для башни полей F ⊆ E ⊆ K, где E ⊆ K алгебраично, выполняется произведение сепарабельных степеней: [E:F]_s [K:E]_s = [K:F]_s.
LaTeX
$$\( \operatorname{finSepDegree}(F,E) \cdot \operatorname{finSepDegree}(E,K) = \operatorname{finSepDegree}(F,K) \)$$
Lean4
/-- If `K / E / F` is a field extension tower, such that `K / E` is algebraic, then their
separable degrees satisfy the tower law
$[E:F]_s [K:E]_s = [K:F]_s$. See also `Module.finrank_mul_finrank`. -/
@[stacks 09HK "Part 1, `finSepDegree` variant"]
theorem finSepDegree_mul_finSepDegree_of_isAlgebraic [Algebra E K] [IsScalarTower F E K] [Algebra.IsAlgebraic E K] :
finSepDegree F E * finSepDegree E K = finSepDegree F K := by
simpa only [Nat.card_prod] using Nat.card_congr (embProdEmbOfIsAlgebraic F E K)
