perfectField_of_isSeparable_of_perfectField_top

English

Combinatorial data of a basis is preserved under exponent-char power maps.

Русский

Комбинаторика базиса сохраняется под отображениями степени q.

LaTeX

$$$\text{basis data preserved under } (\cdot)^{q}$$$

Lean4

/-- If `E / F` is a separable extension, `E` is perfect, then `F` is also perfect. -/
theorem perfectField_of_isSeparable_of_perfectField_top [Algebra.IsSeparable F E] [PerfectField E] : PerfectField F :=
  perfectField_of_perfectClosure_eq_bot F E (perfectClosure.eq_bot_of_isSeparable F E)

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