finSepDegree_bot' — Mathlib

English

For a tower of fields F ⊆ E ⊆ K, the separable degree from F to the bottom intermediate field of E ⊆ K equals the separable degree from F to E.

Русский

В тензоре полей F ⊆ E ⊆ K сепарабельная степень от F до нижнего промежуточного поля (⊥ : IntermediateField E K) равна сепарабельной степени от F до E.

LaTeX

$$$\operatorname{finSepDegree}(F, \bot_E^K) = \operatorname{finSepDegree}(F, E)$$$

Lean4

@[simp]
theorem finSepDegree_bot' : finSepDegree F (⊥ : IntermediateField E K) = finSepDegree F E :=
  finSepDegree_eq_of_equiv _ _ _ ((botEquiv E K).restrictScalars F)

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