exists_factors — Mathlib

English

For any a ≠ 0 in a WfDvdMonoid that is a CommMonoidWithZero, there exists a Multiset f of elements that are all irreducible such that the product of f is associated to a.

Русский

Для любого a ≠ 0 в монойде с нулём, удовлетворяющей условию Well-founded division и являющейся коммоновидной нид, существует мультисет f элементов, все из которых ирредуцируемы, такой что их произведение ассоциировано с a.

LaTeX

$$$\forall a\in\alpha, a \neq 0 \Rightarrow \exists f : \mathrm{Multiset}\ \alpha,\ (\forall b \in f, \mathrm{Irreducible}(b)) \land \mathrm{Associated}(f.prod, a).$$$

Lean4

theorem exists_factors (a : α) : a ≠ 0 → ∃ f : Multiset α, (∀ b ∈ f, Irreducible b) ∧ Associated f.prod a :=
  induction_on_irreducible a (fun h => (h rfl).elim)
    (fun _ hu _ => ⟨0, fun _ h => False.elim (Multiset.notMem_zero _ h), hu.unit, one_mul _⟩) fun a i ha0 hi ih _ =>
    let ⟨s, hs⟩ := ih ha0
    ⟨i ::ₘ s, fun b H => (Multiset.mem_cons.1 H).elim (fun h => h.symm ▸ hi) (hs.1 b),
      by
      rw [s.prod_cons i]
      exact hs.2.mul_left i⟩

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