single_zero_intCast

Mathlib.RingTheory.HahnSeries.Multiplication

URI: https://scilib.ai/kg/mathlib#HahnSeries.single_zero_intCast

English

For any integer z, the Hahn series singleton at 0 with value z cast to R equals z cast.

Русский

Для любого целого z единичная ГансСерия в нулевой степени со значением z, приведённая к R, равна z.

LaTeX

$$$\mathrm{single}(0, z) = z$$$

Lean4

theorem single_zero_intCast [Zero R] [IntCast R] (z : ℤ) : single (0 : Γ) (z : R) = z :=
  rfl

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

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

Разделы

Аффилиация

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