instOfHasExponent — Mathlib

English

Same as HasExponent ⇒ IsPurelyInseparable; the instance provides the implication in the reverse direction.

Русский

То же самое: существование экспоненты порождает чисто неразделимое расширение; экземпляр задаёт это следствие.

LaTeX

$$HasExponent K L ⇒ IsPurelyInseparable K L$$

Lean4

instance [HasExponent K L] : IsPurelyInseparable K L :=
  let ⟨n, h⟩ := ‹HasExponent K L›.has_exponent
  (isPurelyInseparable_iff_pow_mem K (ringExpChar K)).mpr fun x ↦ ⟨n, h x⟩

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