of_integral — Mathlib

English

If F is a field and K is an integral extension with CharZero F, then K is separable over F.

Русский

Если F — поле и K — интегральное расширение над F в характеристике 0, то K разделимо над F.

LaTeX

$$IsSeparable.of_integral (F,K)$$

Lean4

/-- A integral field extension in characteristic 0 is separable. -/
protected instance (priority := 100) of_integral : Algebra.IsSeparable F K :=
  ⟨_root_.IsSeparable.of_integral _⟩

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