intPow_negOfNat_bit1

Mathlib.Tactic.NormNum.Pow

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.NormNum.intPow_negOfNat_bit1

Lean4

theorem intPow_negOfNat_bit1 {b' c' : ℕ} (h1 : Nat.pow a b' = c') (hb : nat_lit 2 * b' + nat_lit 1 = b)
    (hc : c' * (c' * a) = c) : Int.pow (Int.negOfNat a) b = Int.negOfNat c :=
  by
  rw [← hb, Int.negOfNat_eq, Int.negOfNat_eq, Int.pow_eq, pow_succ, pow_mul, neg_pow_two, ← pow_mul, two_mul, pow_add, ←
    hc, ← h1]
  simp [mul_comm, mul_left_comm]

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

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

Разделы

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

Аффилиация

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