rank_mul_insepDegree_of_isPurelyInseparable

English

The same-universe version of the lifted-insep equality: insepDegree E K times rank F E equals insepDegree F K, in the appropriate setting with algebraic extensions.

Русский

Аналог в той же вселенной: insepDegree E K · rank_F E = insepDegree F K.

LaTeX

$$Module.rank F E * insepDegree E K = insepDegree F K$$

Lean4

/-- The same-universe version of `Field.lift_rank_mul_lift_insepDegree_of_isPurelyInseparable`. -/
theorem rank_mul_insepDegree_of_isPurelyInseparable (K : Type v) [Field K] [Algebra F K] [Algebra E K]
    [IsScalarTower F E K] [IsPurelyInseparable F E] : Module.rank F E * insepDegree E K = insepDegree F K := by
  simpa only [Cardinal.lift_id] using lift_rank_mul_lift_insepDegree_of_isPurelyInseparable F E K

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