leval

Mathlib.Algebra.Polynomial.Laurent

URI: https://scilib.ai/kg/mathlib#LaurentPolynomial.leval

← MathLib Explorer

English

smeval(C r · f) = r · smeval(f) holds in the unit context for x ∈ Sˣ.

Русский

smeval(C r · f) = r · smeval(f) выполняется для единиц x ∈ Sˣ.

LaTeX

$$$$ ((C r) * f).smeval x = r \cdot (f.smeval x) $$$$

Lean4

/-- Evaluation as an `R`-linear map. -/
@[simps]
def leval : R[T;T⁻¹] →ₗ[R] S where
  toFun f := f.smeval x
  map_add' f g := smeval_add f g x
  map_smul' r f := by simp [smul_eq_C_mul]

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

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

Разделы

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

Аффилиация

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