eval₂_C

Mathlib.RingTheory.MvPowerSeries.Evaluation

URI: https://scilib.ai/kg/mathlib#MvPowerSeries.eval₂_C

English

For a constant r ∈ R, the evaluation of the constant term under eval₂ φ a is φ(r).

Русский

Для константы r ∈ R значение подстановки константы равно φ(r).

LaTeX

$$$$\operatorname{eval}_{\phi}^{a}(C r) = \phi(r).$$$$

Lean4

@[simp]
theorem eval₂_C (r : R) : eval₂ φ a (C r) = φ r := by rw [← coe_C, eval₂_coe, MvPolynomial.eval₂_C]

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

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

Разделы

Аффилиация

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