of_equiv — Mathlib

English

If K is a field and L is a finite type K-algebra which is unramified, then L is a separable algebra over K.

Русский

Если K — поле, L — конечнопредельная над K алгебра, неразветвленная, то L — сепарабельная над K.

LaTeX

$$$[\text{FormallyUnramified } K L] \Rightarrow [\text{IsSeparable } K L]$$$

Lean4

/-- Being unramified is transported via algebra isomorphisms. -/
theorem of_equiv [Unramified R A] (e : A ≃ₐ[R] B) : Unramified R B
    where
  formallyUnramified := FormallyUnramified.of_equiv e
  finiteType := FiniteType.equiv Unramified.finiteType e

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