isInt_emod

Mathlib.Tactic.NormNum.DivMod

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

Lean4

theorem isInt_emod {a b q m a' : ℤ} {b' r : ℕ} (ha : IsInt a a') (hb : IsNat b b') (hm : q * b' = m) (h : r + m = a')
    (h₂ : Nat.blt r b' = true) : IsNat (a % b) r :=
  ⟨by
    obtain ⟨⟨rfl⟩, ⟨rfl⟩⟩ := ha, hb
    simp only [← h, ← hm, Int.add_mul_emod_self_right]
    rw [Int.emod_eq_of_lt] <;> [simp; simpa using h₂]⟩

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

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

Разделы

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

Аффилиация

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