eval_algebraMap

Mathlib.FieldTheory.RatFunc.AsPolynomial

URI: https://scilib.ai/kg/mathlib#RatFunc.eval_algebraMap

← MathLib Explorer

English

The evaluation of the constant 1 is 1: eval f a 1 = 1.

Русский

Эвальвация константы 1 даёт 1: eval f a 1 = 1.

LaTeX

$$$ \mathrm{eval} f a 1 = 1 $$$

Lean4

@[simp]
theorem eval_algebraMap {S : Type*} [CommSemiring S] [Algebra S K[X]] (p : S) :
    eval f a (algebraMap _ _ p) = (algebraMap _ K[X] p).eval₂ f a := by
  simp [eval, IsScalarTower.algebraMap_apply S K[X] (RatFunc K)]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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