monomial_left_inj

Mathlib.Algebra.MvPolynomial.Basic

URI: https://scilib.ai/kg/mathlib#MvPolynomial.monomial_left_inj

English

If r ≠ 0, then monomial s r = monomial t r if and only if s = t.

Русский

Если r ≠ 0, то monomial s r = monomial t r тогда и только тогда, когда s = t.

LaTeX

$$$ hr : r \neq 0 \rightarrow (monomial\, s\, r = monomial\, t\, r \;\iff\; s = t)$$$

Lean4

@[simp]
theorem monomial_left_inj {s t : σ →₀ ℕ} {r : R} (hr : r ≠ 0) : monomial s r = monomial t r ↔ s = t :=
  Finsupp.single_left_inj hr

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru