ne_bot_of_mem_primesOver — Mathlib

English

If p ≠ ⊥ and P lies over p (P ∈ p.primesOver S), then P ≠ ⊥.

Русский

Если p ≠ ⊥ и P лежит над p, то P ≠ ⊥.

LaTeX

$$$hp: p \neq 0 \Rightarrow P \neq 0$ for P ∈ p.primesOver S$$

Lean4

theorem ne_bot_of_mem_primesOver {S : Type*} [Ring S] [Algebra R S] [Nontrivial S] [NoZeroSMulDivisors R S]
    {p : Ideal R} (hp : p ≠ ⊥) {P : Ideal S} (hP : P ∈ p.primesOver S) : P ≠ ⊥ :=
  @ne_bot_of_liesOver_of_ne_bot _ _ _ _ _ _ _ _ hp P hP.2

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