monomial_one_dvd_monomial_one — Mathlib

English

For all σ, i, j, monomial i 1 divides monomial j 1 if and only if i ≤ j (assuming R is nontrivial).

Русский

Для всех σ, i, j мономиал i единица делит мономиал j единица тогда и только тогда, когда i ≤ j (при условии ненулевого кольца).

LaTeX

$$$$ \\text{monomial}(i,1) \\mid \\text{monomial}(j,1) \\iff i \\le j, \\quad [\\text{R nontrivial}]. $$$$

Lean4

@[simp]
theorem monomial_one_dvd_monomial_one [Nontrivial R] {i j : σ →₀ ℕ} : monomial i (1 : R) ∣ monomial j 1 ↔ i ≤ j :=
  by
  rw [monomial_dvd_monomial]
  simp_rw [one_ne_zero, false_or, dvd_rfl, and_true]

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