IsUnramifiedIn — Mathlib

English

An infinite place w of the base field k is unramified in K if every infinite place of K lying over w is unramified over k.

Русский

Бесконечное место w базового поля k безразветвлено в K, если каждый бесконечный путь над w в K безразветвлён над k.

LaTeX

$$\\IsUnramifiedIn(k, w) := ∀ v, \\comap v (algebraMap k K) = w \\Rightarrow \\IsUnramified(k, v).$$

Lean4

/-- A infinite place of the base field is unramified in a field extension if every
infinite place over it is unramified. -/
def IsUnramifiedIn (w : InfinitePlace k) : Prop :=
  ∀ v, comap v (algebraMap k K) = w → IsUnramified k v

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