eval_C

Mathlib.FieldTheory.RatFunc.AsPolynomial

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

English

For any c ∈ K, evaluating the constant C c yields f c: eval f a (C c) = f c.

Русский

Для любого c ∈ K при_eval константы C c даёт f c: eval f a (C c) = f c.

LaTeX

$$$ \mathrm{eval} f a (\mathrm{C} c) = f c $$$

Lean4

@[simp]
theorem eval_C {c : K} : eval f a (C c) = f c := by simp [eval]

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

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

Разделы

Аффилиация

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