σ : Type u_2
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ →₀ ℕ
⊢ (1 = 0 ∨ i ≤ j) ∧ 1 ∣ 1 ↔ i ≤ j
σ : Type u_2
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ →₀ ℕ
⊢ ↑(monomial i) 1 ∣ ↑(monomial j) 1 ↔ i ≤ j
rw [monomial_dvd_monomial]
no goals
σ : Type u_2
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ →₀ ℕ
⊢ (1 = 0 ∨ i ≤ j) ∧ 1 ∣ 1 ↔ i ≤ j
simp_rw [one_ne_zero, false_or_iff, dvd_rfl, and_true_iff]