English
For monomials monomial i r and monomial j s in the MV polynomial algebra, monomial i r divides monomial j s if and only if (s = 0 or i ≤ j) and r divides s.
Русский
Для мономиалов monomial i r и monomial j s в MV-полиномном алгебре, monomial i r делит monomial j s тогда и только тогда, когда (s = 0 или i ≤ j) и r делит s.
LaTeX
$$$$ \\text{monomial}(i,r) \\mid \\text{monomial}(j,s) \\iff (s = 0 \\lor i \\le j) \\land (r \\mid s). $$$$
Lean4
theorem monomial_dvd_monomial {r s : R} {i j : σ →₀ ℕ} : monomial i r ∣ monomial j s ↔ (s = 0 ∨ i ≤ j) ∧ r ∣ s :=
by
constructor
· rintro ⟨x, hx⟩
rw [MvPolynomial.ext_iff] at hx
have hj := hx j
have hi := hx i
classical
simp_rw [coeff_monomial, if_pos] at hj hi
simp_rw [coeff_monomial_mul'] at hi hj
split_ifs at hj with hi
· exact ⟨Or.inr hi, _, hj⟩
· exact ⟨Or.inl hj, hj.symm ▸ dvd_zero _⟩
· rintro ⟨h | hij, d, rfl⟩
· simp_rw [h, monomial_zero, dvd_zero]
· refine ⟨monomial (j - i) d, ?_⟩
rw [monomial_mul, add_tsub_cancel_of_le hij]
