isSeparable_iff_finInsepDegree_eq_one

English

An algebra is separable over F iff finInsepDegree F K = 1.

Русский

Алгебра над F является сепарабельной тогда и только тогда, когда finInsepDegree F K = 1.

LaTeX

$$$\text{Algebra.IsSeparable } F K \iff \operatorname{finInsepDegree} F K = 1$$$

Lean4

theorem isSeparable_iff_finInsepDegree_eq_one : Algebra.IsSeparable F K ↔ finInsepDegree F K = 1 := by
  rw [← separableClosure.eq_top_iff, ← IntermediateField.finrank_eq_one_iff_eq_top, finInsepDegree]

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