mem_normalizedFactors_iff — Mathlib

English

For a maximal p, membership in primesOver A corresponds to membership in the normalizedFactors of the mapped p.

Русский

Для максимального p члены множества primesOver A эквивалентны членству в нормализованных факторах образованного p.

LaTeX

$$$P \in p.primesOver A \iff P \in \mathrm{normalizedFactors}(\mathrm{Ideal.map}(\mathrm{algebraMap}\,R\,A) p)$$$

Lean4

nonrec theorem mem_normalizedFactors_iff {p I : Ideal A} (hI : I ≠ ⊥) : p ∈ normalizedFactors I ↔ p.IsPrime ∧ I ≤ p :=
  by
  rw [← Ideal.dvd_iff_le]
  by_cases hp : p = 0
  · rw [← zero_eq_bot] at hI
    simp only [hp, zero_notMem_normalizedFactors, zero_dvd_iff, hI, false_iff, not_and, not_false_eq_true, implies_true]
  · rwa [mem_normalizedFactors_iff hI, prime_iff_isPrime]

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