invUnitsSub_mul_X

Mathlib.RingTheory.PowerSeries.WellKnown

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

English

Multiplying invUnitsSub u by X equals invUnitsSub u times (u) evaluated minus 1.

Русский

Умножение invUnitsSub(u) на X равно invUnitsSub(u) умноженному на C(u) минус 1.

LaTeX

$$$invUnitsSub(u) \cdot X = invUnitsSub(u) \cdot C(u) - 1$$$

Lean4

@[simp]
theorem invUnitsSub_mul_X (u : Rˣ) : invUnitsSub u * X = invUnitsSub u * C (u : R) - 1 :=
  by
  ext (_ | n)
  · simp
  · simp [pow_succ']

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

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

Разделы

Аффилиация

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