toFinsupp_injective

Mathlib.Algebra.Polynomial.Basic

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

English

The map toFinsupp : R[X] → AddMonoidAlgebra _ _ is injective.

Русский

Отображение toFinsupp: R[X] → AddMonoidAlgebra является инъективным.

LaTeX

$$Function.Injective\$toFinsupp\$$$

Lean4

theorem toFinsupp_injective : Function.Injective (toFinsupp : R[X] → AddMonoidAlgebra _ _) := fun ⟨_x⟩ ⟨_y⟩ =>
  congr_arg _

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

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

Разделы

Аффилиация

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