prod_dvd_iff' — Mathlib

English

Let u be a prime multiset and n ∈ ℕ+. Then prod(u) divides n if and only if u ≤ n.factorMultiset.

Русский

Пусть u — мультсет простых и n ∈ ℕ+. Тогда prod(u) делит n тогда и только тогда, когда u ≤ factorMultiset(n).

LaTeX

$$$ \\operatorname{prod}(u) \\mid n \\iff u \\le n.\\operatorname{factorMultiset} $$$

Lean4

theorem prod_dvd_iff' {u : PrimeMultiset} {n : ℕ+} : u.prod ∣ n ↔ u ≤ n.factorMultiset :=
  by
  let h := @prod_dvd_iff u n.factorMultiset
  rw [n.prod_factorMultiset] at h
  exact h

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