run

Mathlib.Tactic.NormNum.Pow

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

Lean4

theorem run (p : IsNatPowT (Nat.pow a (nat_lit 1) = a) a b c) : Nat.pow a b = c :=
  p.run' (Nat.pow_one _)

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

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

Разделы

Аффилиация

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