isPurelyInseparable — Mathlib

English

If L/K is p-radical, then L/K is purely inseparable; in particular, if L is perfect, then IsPerfectClosure K L holds.

Русский

Если L/k - p-радикальное, то расщепление чисто неразделимо; в частности, если L совершено, то IsPerfectClosure K L выполняется.

LaTeX

$$$ IsPurelyInseparable\ K\ L \;\;\; \text{from } IsPRadical(\mathrm{algebraMap}\ K L, p) $$$

Lean4

/-- If `L / K` is a `p`-radical field extension, then it is purely inseparable. -/
theorem isPurelyInseparable [IsPRadical (algebraMap K L) p] : IsPurelyInseparable K L :=
  (isPurelyInseparable_iff_pow_mem K p).2 (IsPRadical.pow_mem (algebraMap K L) p)

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