trans — Mathlib

English

Unramified-ness is transitive along a tower of fields: if k ⊆ K and K ⊆ F with the respective unramified-at-infinite-places properties, then k ⊆ F is unramified at infinite places.

Русский

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

LaTeX

$$trans IsUnramifiedAtInfinitePlaces k K, IsUnramifiedAtInfinitePlaces K F ⇒ IsUnramifiedAtInfinitePlaces k F$$

Lean4

theorem trans [h₁ : IsUnramifiedAtInfinitePlaces k K] [h₂ : IsUnramifiedAtInfinitePlaces K F] :
    IsUnramifiedAtInfinitePlaces k F where
  isUnramified w := Eq.trans (IsScalarTower.algebraMap_eq k K F ▸ h₁.1 (w.comap (algebraMap _ _))) (h₂.1 w)

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