invUnitsSub_mul_sub

Mathlib.RingTheory.PowerSeries.WellKnown

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

English

For any unit u, invUnitsSub u multiplied by (C(u) - X) equals 1.

Русский

Для любого элемента-единицы u invUnitsSub(u) умноженное на (C(u) - X) равно 1.

LaTeX

$$invUnitsSub(u) * (C(u) - X) = 1$$

Lean4

@[simp]
theorem invUnitsSub_mul_sub (u : Rˣ) : invUnitsSub u * (C (u : R) - X) = 1 := by simp [mul_sub, sub_sub_cancel]

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

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

Разделы

Аффилиация

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