instCoeFunForall

Mathlib.RingTheory.PolynomialLaw.Basic

URI: https://scilib.ai/kg/mathlib#PolynomialLaw.instCoeFunForall

English

The function-coercion from polynomial laws to ordinary functions is given by ground.

Русский

Приведение полиномального закона к обычной функции задаётся через ground.

LaTeX

$$$\\text{coe}_{M,N,R} : (M \\to_{p\\ell[R]} N) \\to (M \\to N) \\\\text{ defined by } f \\mapsto f.ground.$$$

Lean4

instance : CoeFun (M →ₚₗ[R] N) (fun _ ↦ M → N) where coe := ground

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

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

Разделы

Аффилиация

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