bot — Mathlib

English

If F is unramified over k at infinite places and K/F is algebraic, then k is unramified over K at infinite places.

Русский

Если F безразветвлено над k на бесконечных местах, и K/F алгебраическое, то k безразветвлено над K на бесконечных местах.

LaTeX

$$bottom IsUnramifiedAtInfinitePlaces k F, Algebra.IsAlgebraic K F ⇒ IsUnramifiedAtInfinitePlaces k K$$

Lean4

theorem bot [h₁ : IsUnramifiedAtInfinitePlaces k F] [Algebra.IsAlgebraic K F] : IsUnramifiedAtInfinitePlaces k K where
  isUnramified
    w := by
    obtain ⟨w, rfl⟩ := InfinitePlace.comap_surjective (K := F) w
    exact (h₁.1 w).comap K

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