intPow_negOfNat_bit0

Mathlib.Tactic.NormNum.Pow

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

Lean4

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

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

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

Разделы

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

Аффилиация

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