u : PrimeMultiset
n : ℕ+
h : prod u ∣ prod (PNat.factorMultiset n) ↔ u ≤ PNat.factorMultiset n := prod_dvd_iff
⊢ prod u ∣ n ↔ u ≤ PNat.factorMultiset n
u : PrimeMultiset
n : ℕ+
⊢ prod u ∣ n ↔ u ≤ PNat.factorMultiset n
let h := @prod_dvd_iff u n.factorMultiset
u : PrimeMultiset
n : ℕ+
h : prod u ∣ n ↔ u ≤ PNat.factorMultiset n
⊢ prod u ∣ n ↔ u ≤ PNat.factorMultiset n
u : PrimeMultiset
n : ℕ+
h : prod u ∣ prod (PNat.factorMultiset n) ↔ u ≤ PNat.factorMultiset n := prod_dvd_iff
⊢ prod u ∣ n ↔ u ≤ PNat.factorMultiset n
rw [n.prod_factorMultiset] at h
no goals
u : PrimeMultiset
n : ℕ+
h : prod u ∣ n ↔ u ≤ PNat.factorMultiset n
⊢ prod u ∣ n ↔ u ≤ PNat.factorMultiset n
exact h