isPurelyInseparable — Mathlib

English

The relative perfect closure is purely inseparable over F by construction.

Русский

Относительное совершенное замыкание построено так, что над F оно чисто бесразделимо.

LaTeX

$$perfectClosure isPurelyInseparable$$

Lean4

/-- The relative perfect closure of `F` in `E` is purely inseparable over `F`. -/
instance isPurelyInseparable : IsPurelyInseparable F (perfectClosure F E) :=
  by
  rw [isPurelyInseparable_iff_pow_mem F (ringExpChar F)]
  exact fun ⟨_, n, y, h⟩ ↦ ⟨n, y, (algebraMap _ E).injective h⟩

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