top — Mathlib

English

If k ⊆ F has unramified infinite places and K/F is an extension, then K/k inherits a compatible unramified-at-infinite-places structure.

Русский

Если у пары полей k ⊆ F безразветвленность на бесконечных местах, и K/F — расширение, то K/k наследует совместную структуру безразветвленности на бесконечных местах.

LaTeX

$$top IsUnramifiedAtInfinitePlaces k F ⇒ IsUnramifiedAtInfinitePlaces K F$$

Lean4

theorem top [h : IsUnramifiedAtInfinitePlaces k F] : IsUnramifiedAtInfinitePlaces K F where
  isUnramified w := (h.1 w).of_restrictScalars K

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