monomial_eq_monomial_iff — Mathlib

English

Two monomials are equal iff either exponents and coefficients match, or both coefficients are zero.

Русский

Два мономиала равны тогда и только тогда, когда либо степени и коэффициенты совпадают, либо оба коэффициента равны нулю.

LaTeX

$$$\operatorname{monomial}(m,a) = \operatorname{monomial}(n,b) \iff (m=n \wedge a=b) \lor (a=0 \wedge b=0)$$$

Lean4

theorem monomial_eq_monomial_iff {m n : ℕ} {a b : R} : monomial m a = monomial n b ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0 := by
  rw [← toFinsupp_inj, toFinsupp_monomial, toFinsupp_monomial, Finsupp.single_eq_single_iff]

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