finSepDegree_bot — Mathlib

English

Let F be a field and E an extension with the bottom intermediate field ⊥ in F E. Then the separable degree of the extension F → (⊥ : IntermediateField F E) is 1.

Русский

Пусть F — поле и E — расширение, а ⊥ обозначает нижнее подполе в составе F E. Тогда сепарабельная степень расширения F → (⊥) равна 1.

LaTeX

$$$\operatorname{finSepDegree}(F, \perp) = 1$$$

Lean4

@[simp]
theorem finSepDegree_bot : finSepDegree F (⊥ : IntermediateField F E) = 1 := by
  rw [finSepDegree_eq_of_equiv _ _ _ (botEquiv F E), finSepDegree_self]

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