English
If the map algebraMap K L is p-radical, then L/K is purely inseparable.
Русский
Если алгебра-пользователь K→L является p-радикальным, то L/K чисто неразделимо.
LaTeX
$$$ IsPRadical(\mathrm{algebraMap}\ K L, p) \Rightarrow IsPurelyInseparable K L $$$
Lean4
/-- If `L / K` is a purely inseparable field extension, then it is `p`-radical. In particular, if
`L` is perfect, then the (relative) perfect closure `perfectClosure K L` is a perfect closure
of `K`, that is, `IsPerfectClosure (algebraMap K (perfectClosure K L)) p`. -/
instance isPRadical [IsPurelyInseparable K L] : IsPRadical (algebraMap K L) p
where
pow_mem' := (isPurelyInseparable_iff_pow_mem K p).1 ‹_›
ker_le' := (RingHom.injective_iff_ker_eq_bot _).1 (algebraMap K L).injective ▸ bot_le
