map_id

Mathlib.Algebra.Polynomial.Eval.Coeff

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

English

Applying the identity ring homomorphism to a polynomial leaves the polynomial unchanged: p.map(id) = p.

Русский

Применение тождественного гомоморфизма к полиномy не меняет полином: p.map(id) = p.

LaTeX

$$$p.map(\\mathrm{id}) = p$$$

Lean4

@[simp]
theorem map_id : p.map (RingHom.id _) = p := by simp [Polynomial.ext_iff, coeff_map]

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

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

Разделы

Аффилиация

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