insepDegree_mul_insepDegree_of_isAlgebraic

English

The finitary version of the tower law for inseparable degrees: finInsepDegree F E · finInsepDegree E K = finInsepDegree F K, when E/F is algebraic.

Русский

Конечная версия закона башни для инsep-степеней: finInsepDegree F E · finInsepDegree E K = finInsepDegree F K, если E/F алгебраично.

LaTeX

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

Lean4

/-- The same-universe version of `Field.lift_insepDegree_mul_lift_insepDegree_of_isAlgebraic`. -/
@[stacks 09HK "Part 2"]
theorem insepDegree_mul_insepDegree_of_isAlgebraic (K : Type v) [Field K] [Algebra F K] [Algebra E K]
    [IsScalarTower F E K] [Algebra.IsAlgebraic F E] : insepDegree F E * insepDegree E K = insepDegree F K := by
  simpa only [Cardinal.lift_id] using lift_insepDegree_mul_lift_insepDegree_of_isAlgebraic F E K

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