isPrime — Mathlib

English

For a prime factor P of the image of p in the target, the corresponding ideal P is nonzero.

Русский

Для простого множителя P образа p в целевом кольце соответствующий идеал P ненулевой.

LaTeX

$$$\\\\(P : (\\\\text{factors} (\\\\operatorname{map} (\\\\operatorname{algebraMap} R S) p)).toFinset) \\\\text{prime factor} \\rightarrow P \\\\neq ⊥$$$

Lean4

instance isPrime (P : (factors (map (algebraMap R S) p)).toFinset) : IsPrime (P : Ideal S) :=
  Ideal.isPrime_of_prime (prime_of_factor _ (Multiset.mem_toFinset.mp P.2))

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