mem_normalizedFactors_iff — Mathlib

English

For polynomials over a field, and any q ≠ 0, p belongs to the multiset of normalized factors of q if and only if p is irreducible, monic, and p divides q.

Русский

Для многочленов над полем и любого q ≠ 0, p принадлежит множеству нормализованных факторов q тогда и только тогда, когда p неприводим, моничен и p делит q.

LaTeX

$$$p \in normalizedFactors(q) \iff \text{Irreducible}(p) \wedge p.Monic \wedge p \mid q$.$$

Lean4

protected theorem mem_normalizedFactors_iff [DecidableEq R] (hq : q ≠ 0) :
    p ∈ normalizedFactors q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q :=
  by
  by_cases hp : p = 0
  · simpa [hp] using zero_notMem_normalizedFactors _
  · rw [mem_normalizedFactors_iff' hq, normalize_eq_self_iff_monic hp]

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