comp — Mathlib

English

If p ⊂ A and its lie over P ⊂ B, and both p and P are prime and unramified over R and A respectively, then P is unramified over R.

Русский

Если p ⊂ A и P ⊂ B лежит над p, и оба являются простыми и неразветвленными над R и A соответственно, то P неразветвлен над R.

LaTeX

$$IsUnramifiedAt.comp p P$$

Lean4

theorem comp (p : Ideal A) (P : Ideal B) [P.LiesOver p] [p.IsPrime] [P.IsPrime] [IsUnramifiedAt R p]
    [IsUnramifiedAt A P] : IsUnramifiedAt R P :=
  by
  have : FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime P) := .of_comp A _ _
  exact FormallyUnramified.comp R (Localization.AtPrime p) _

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