isInt_emod_neg

Mathlib.Tactic.NormNum.DivMod

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

Lean4

theorem isInt_emod_neg {a b : ℤ} {r : ℕ} (h : IsNat (a % -b) r) : IsNat (a % b) r :=
  ⟨by rw [← Int.emod_neg, h.out]⟩

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

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

Разделы

Аффилиация

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