laurent_algebraMap

Mathlib.FieldTheory.Laurent

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

English

laurent r (algebraMap p) = algebraMap (taylor r p).

Русский

laurent r (algebraMap p) = algebraMap (taylor r p).

LaTeX

$$$\\mathrm{laurent\\_algebraMap} : \\mathrm{laurent}\\_r(\\text{algebraMap}~p) = \\text{algebraMap}(\\operatorname{taylor}(r)p).$$$

Lean4

@[simp]
theorem laurent_algebraMap : laurent r (algebraMap _ _ p) = algebraMap _ _ (taylor r p) :=
  laurentAux_algebraMap _ _

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

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

Разделы

Аффилиация

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