mk — Mathlib · SciLib

English

If P is a prime ideal of B lying over p, then P maps to an element of primesOver p B.

Русский

Если P — простой идеал B, лежащий над p, то P соответствует элементу primesOver p B.

LaTeX

$$mk : (P:Ideal B) → [hPp: P.IsPrime] → [hp: P.LiesOver p] → (p.primesOver B).Elem$$

Lean4

/-- If an ideal `P` of `B` is prime and lying over `p`, then it is in `primesOver p B`. -/
abbrev mk (P : Ideal B) [hPp : P.IsPrime] [hp : P.LiesOver p] : primesOver p B :=
  ⟨P, ⟨hPp, hp⟩⟩

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