instDecidableEq

Mathlib.Algebra.Polynomial.Basic

URI: https://scilib.ai/kg/mathlib#Polynomial.instDecidableEq

English

If R has decidable equality, then the polynomial ring R[X] also has decidable equality.

Русский

Если в R есть разрешимость равенства (DecidableEq), то и в R[X] она существует.

LaTeX

$$[\text{DecidableEq } R] \Rightarrow [\text{DecidableEq } (R[X])]$$

Lean4

instance [DecidableEq R] : DecidableEq R[X] :=
  @Equiv.decidableEq R[X] _ (toFinsuppIso R).toEquiv (Finsupp.instDecidableEq)

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

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

Разделы

Аффилиация

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