sepDegree_mul_sepDegree_of_isAlgebraic

English

The same-universe version of the tower rule for separable degrees under algebraicity: lift(sepDegree F E) · lift(sepDegree E K) = lift(sepDegree F K).

Русский

Тот же закон башни для сепарабельных степеней в рамках алгебраичности: lift(sepDegree F E) · lift(sepDegree E K) = lift(sepDegree F K).

LaTeX

$$Cardinal.lift(sepDegree F E) · Cardinal.lift(sepDegree E K) = Cardinal.lift(sepDegree F K)$$

Lean4

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

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