trans

Mathlib.Tactic.NormNum.PowMod

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

Lean4

theorem trans (h1 : IsNatPowModT p a b m c) (h2 : IsNatPowModT (Nat.mod (Nat.pow a b) m = c) a b' m c') :
    IsNatPowModT p a b' m c' :=
  ⟨h2.run' ∘ h1.run'⟩

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

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

Разделы

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

Аффилиация

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