factorization_le_iff_dvd — Mathlib

English

Same statement as above: for nonzero a,b, (a·b).factorization = a.factorization + b.factorization.

Русский

То же самое: для ненулевых a,b, факторизация ab равна сумме факторизаций.

LaTeX

$$$ (a \\cdot b).factorization = a.factorization + b.factorization \\quad (a \\neq 0,\\; b \\neq 0)$$$

Lean4

theorem factorization_le_iff_dvd {d n : ℕ} (hd : d ≠ 0) (hn : n ≠ 0) : d.factorization ≤ n.factorization ↔ d ∣ n :=
  by
  constructor
  · intro hdn
    set K := n.factorization - d.factorization with hK
    use K.prod (· ^ ·)
    rw [← factorization_prod_pow_eq_self hn, ← factorization_prod_pow_eq_self hd, ←
      Finsupp.prod_add_index' pow_zero pow_add, hK, add_tsub_cancel_of_le hdn]
  · rintro ⟨c, rfl⟩
    rw [factorization_mul hd (right_ne_zero_of_mul hn)]
    simp

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