C_inj

Mathlib.Algebra.MvPolynomial.Basic

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

English

(C r) = (C s) ↔ r = s, in general for σ, R.

Русский

(C r) = (C s) ↔ r = s, в общем виде для σ, R.

LaTeX

$$$ (C (r) = C (s)) \iff r = s $$$

Lean4

@[simp]
theorem C_inj {σ : Type*} (R : Type*) [CommSemiring R] (r s : R) : (C r : MvPolynomial σ R) = C s ↔ r = s :=
  (C_injective σ R).eq_iff

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

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

Разделы

Аффилиация

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