coe_mapRingHom

Mathlib.Algebra.Polynomial.Eval.Defs

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

English

The coercion of mapRingHom(f) equals the map f: the underlying function is map f.

Русский

Приведение mapRingHom(f) имеет значения, равные map f: базовая функция равна map f.

LaTeX

$$$$\\mathrm{coe}(\\mathrm{mapRingHom}(f)) = \\mathrm{map}(f)$$$$

Lean4

@[simp]
theorem coe_mapRingHom (f : R →+* S) : ⇑(mapRingHom f) = map f :=
  rfl

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

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

Разделы

Аффилиация

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