instCSLiftValPNatNatHMul

Mathlib.Tactic.Ring.PNat

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

Lean4

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

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

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

Разделы

Аффилиация

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