isInt_ediv

Mathlib.Tactic.NormNum.DivMod

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

Lean4

theorem isInt_ediv {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) : IsInt (a / b) q :=
  ⟨by
    obtain ⟨⟨rfl⟩, ⟨rfl⟩⟩ := ha, hb
    simp only [Nat.blt_eq] at h₂; simp only [← h, ← hm, Int.cast_id]
    rw [Int.add_mul_ediv_right _ _ (Int.ofNat_ne_zero.2 ((Nat.zero_le ..).trans_lt h₂).ne')]
    rw [Int.ediv_eq_zero_of_lt, zero_add] <;> [simp; simpa using h₂]⟩

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

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

Разделы

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

Аффилиация

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