IsUnramified — Mathlib

English

An infinite place w is unramified in the extension if the restricted multiplicity equals the original multiplicity.

Русский

Бесконечное место нерасслоено при расширении, если ограниченная кратность равна исходной.

LaTeX

$$$ \operatorname{mult}(w.\mathrm{comap}(\mathrm{algebraMap}_{kK})) = \operatorname{mult}(w) $$$

Lean4

/-- An infinite place is unramified in a field extension if the restriction has the same multiplicity.
-/
def IsUnramified : Prop :=
  mult (w.comap (algebraMap k K)) = mult w

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