isNat_ratDen

Mathlib.Tactic.NormNum.GCD

URI: https://scilib.ai/kg/mathlib#Tactic.NormNum.isNat_ratDen

Lean4

theorem isNat_ratDen : ∀ {q : ℚ} {n : ℤ} {n' : ℕ} {d : ℕ}, IsRat q n d → n.natAbs = n' → n'.gcd d = 1 → IsNat q.den d
  | _, n, _, d, ⟨hi, rfl⟩, rfl, h => by
    constructor
    have : 0 < d := Nat.pos_iff_ne_zero.mpr <| by simpa using hi.ne_zero
    simp_rw [Rat.mul_den, Rat.den_intCast, invOf_eq_inv, Rat.inv_natCast_den_of_pos this,
      Rat.inv_natCast_num_of_pos this, Rat.num_intCast, one_mul, mul_one, Nat.cast_id, h, Nat.div_one]

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

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

Разделы

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

Аффилиация

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