coeff_invUnitsSub

Mathlib.RingTheory.PowerSeries.WellKnown

URI: https://scilib.ai/kg/mathlib#PowerSeries.coeff_invUnitsSub

English

The coefficient of degree n in invUnitsSub u is 1 divided by u^(n+1).

Русский

Коэффициент степени n у invUnitsSub(u) равен 1 на u^(n+1).

LaTeX

$$$\text{coeff}_n(\mathrm{invUnitsSub}\,u) = 1 /_p u^{n+1}$$$

Lean4

@[simp]
theorem coeff_invUnitsSub (u : Rˣ) (n : ℕ) : coeff n (invUnitsSub u) = 1 /ₚ u ^ (n + 1) :=
  coeff_mk _ _

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

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

Разделы

Аффилиация

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