monomial_one_eq_iff — Mathlib

English

In a nontrivial ring, monomials with coefficient 1 are distinct: monomial i with coefficient 1 equals monomial j with coefficient 1 if and only if i = j.

Русский

В не тривиальном кольце мононимиалы с коэффициентом 1 различны: monomial i 1 = monomial j 1 ⇔ i = j.

LaTeX

$$$\operatorname{monomial}(i,1) = \operatorname{monomial}(j,1) \iff i=j.$$$

Lean4

theorem monomial_one_eq_iff [Nontrivial R] {i j : ℕ} : (monomial i 1 : R[X]) = monomial j 1 ↔ i = j :=
  by
  simp_rw [← ofFinsupp_single, ofFinsupp.injEq]
  exact AddMonoidAlgebra.of_injective.eq_iff

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