English
If q and r have nonzero denominators in α, then the product respects the embedding: ↑(q · r) = (↑q)(↑r).
Русский
Если знаменатели q и r ненулевые в α, то произведение сохраняется через вложение: ↑(q · r) = (↑q)(↑r).
LaTeX
$$$ (q \cdot r)^{\uparrow} = (q^{\uparrow})(r^{\uparrow}) $$$
Lean4
@[norm_cast]
theorem cast_divNat_of_ne_zero (a : ℕ) {b : ℕ} (hb : (b : α) ≠ 0) : divNat a b = (a / b : α) :=
by
rcases e : divNat a b with ⟨⟨n, d, h, c⟩, hn⟩
rw [← Rat.num_nonneg] at hn
lift n to ℕ using hn
have hd : (d : α) ≠ 0 := by
refine fun hd ↦ hb ?_
have : Rat.divInt a b = _ := congr_arg NNRat.cast e
obtain ⟨k, rfl⟩ : d ∣ b := by simpa [Int.natCast_dvd_natCast, this] using Rat.den_dvd a b
simp [*]
have hb' : b ≠ 0 := by rintro rfl; exact hb Nat.cast_zero
simp_rw [Rat.mk'_eq_divInt, mk_divInt, divNat_inj hb' h] at e
rw [cast_def]
dsimp
rw [Commute.div_eq_div_iff _ hd hb]
· norm_cast
rw [e]
exact b.commute_cast _
