trans

Mathlib.Tactic.NormNum.Pow

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

Lean4

/-- This is the key to making the proof proceed as a balanced tree of applications instead of
a linear sequence. It is just modus ponens after unwrapping the definitions. -/
theorem trans {p : Prop} {b' c' : ℕ} (h1 : IsNatPowT p a b c) (h2 : IsNatPowT (Nat.pow a b = c) a b' c') :
    IsNatPowT p a b' c' :=
  ⟨h2.run' ∘ h1.run'⟩

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

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

Разделы

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

Аффилиация

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