σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
j : σ →₀ ℕ
r : R
⊢ (r = 0 ∨ Finsupp.single i 1 ≤ j) ∧ 1 ∣ r ↔ r = 0 ∨ ↑j i ≠ 0
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
j : σ →₀ ℕ
r : R
⊢ X i ∣ ↑(monomial j) r ↔ r = 0 ∨ ↑j i ≠ 0
refine' monomial_dvd_monomial.trans _
no goals
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
j : σ →₀ ℕ
r : R
⊢ (r = 0 ∨ Finsupp.single i 1 ≤ j) ∧ 1 ∣ r ↔ r = 0 ∨ ↑j i ≠ 0
simp_rw [one_dvd, and_true_iff, Finsupp.single_le_iff, Nat.one_le_iff_ne_zero]