instCSLiftValPNatNatHPow

Mathlib.Tactic.Ring.PNat

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Ring.instCSLiftValPNatNatHPow

Lean4

instance {n n' k} [h1 : CSLiftVal (n : ℕ+) n'] : CSLiftVal (n ^ k) (n' ^ k) :=
  ⟨by simp [h1.1, CSLift.lift]⟩

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

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

Разделы

Аффилиация

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