exists_mem_normalizedFactors_of_dvd

English

If a ≠ 0 and p is irreducible and p ∣ a, then there exists q ∈ normalizedFactors a with p ∼ q.

Русский

Если a ≠ 0 и p неразложимо и p делит a, тогда существует q ∈ normalizedFactors a такое, что p ассоциировано с q.

LaTeX

$$p ∣ a → ∃ q ∈ normalizedFactors a, p ~ᵤ q$$

Lean4

theorem exists_mem_normalizedFactors_of_dvd {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) :
    p ∣ a → ∃ q ∈ normalizedFactors a, p ~ᵤ q := fun ⟨b, hb⟩ =>
  have hb0 : b ≠ 0 := fun hb0 => by simp_all
  have : Multiset.Rel Associated (p ::ₘ normalizedFactors b) (normalizedFactors a) :=
    factors_unique
      (fun _ hx => (Multiset.mem_cons.1 hx).elim (fun h => h.symm ▸ hp) (irreducible_of_normalized_factor _))
      irreducible_of_normalized_factor
      (Associated.symm <|
        calc
          Multiset.prod (normalizedFactors a) ~ᵤ a := prod_normalizedFactors ha0
          _ = p * b := hb
          _ ~ᵤ Multiset.prod (p ::ₘ normalizedFactors b) :=
            by
            rw [Multiset.prod_cons]
            exact (prod_normalizedFactors hb0).symm.mul_left _)
  Multiset.exists_mem_of_rel_of_mem this (by simp)

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