negOnePow_sub

Mathlib.Algebra.Ring.NegOnePow

URI: https://scilib.ai/kg/mathlib#Int.negOnePow_sub

← MathLib Explorer

English

For all n1, n2 in ℤ, (n1 - n2).negOnePow = n1.negOnePow * n2.negOnePow.

Русский

Для всех n1, n2 ∈ ℤ, (n1 - n2).negOnePow = n1.negOnePow * n2.negOnePow.

LaTeX

$$$(n_1 - n_2).negOnePow = n_1.negOnePow \cdot n_2.negOnePow$$$

Lean4

theorem negOnePow_sub (n₁ n₂ : ℤ) : (n₁ - n₂).negOnePow = n₁.negOnePow * n₂.negOnePow := by
  simp only [sub_eq_add_neg, negOnePow_add, negOnePow_neg]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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