C

Mathlib.RingTheory.PowerSeries.Restricted

URI: https://scilib.ai/kg/mathlib#PowerSeries.IsRestricted.C

English

The constant series with value a, i.e. C a, is restricted for any a ∈ R and parameter c.

Русский

Постоянный ряд с коэффициентом a, то есть C a, ограничен по c.

LaTeX

$$$\mathrm{IsRestricted}(c, \mathrm{C\; }a)$$$

Lean4

theorem C (a : R) : IsRestricted c (C a) := by simpa [monomial_zero_eq_C_apply] using monomial c 0 a

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

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

Разделы

Аффилиация

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