fract_div_natCast_eq_div_natCast_mod

English

For m ∈ ℤ and n ∈ ℕ with n ≠ 0, fract((m/n)) = (m mod n)/n (with the appropriate casts).

Русский

Для m ∈ ℤ и n ∈ ℕ, n ≠ 0: fract((m/n)) = (m mod n)/n (с приведениями к тем же полям).

LaTeX

$$$\\\\operatorname{fract}(\\\\frac{m}{n}) = \\\\frac{m \\\\bmod n}{n}$$$

Lean4

theorem fract_div_natCast_eq_div_natCast_mod {m n : ℕ} : fract ((m : k) / n) = ↑(m % n) / n :=
  by
  rcases n.eq_zero_or_pos with (rfl | hn)
  · simp
  have hn' : 0 < (n : k) := by norm_cast
  refine fract_eq_iff.mpr ⟨?_, ?_, m / n, ?_⟩
  · positivity
  · simpa only [div_lt_one hn', Nat.cast_lt] using m.mod_lt hn
  · rw [sub_eq_iff_eq_add', ← mul_right_inj' hn'.ne', mul_div_cancel₀ _ hn'.ne', mul_add, mul_div_cancel₀ _ hn'.ne']
    norm_cast
    rw [← Nat.cast_add, Nat.mod_add_div m n]

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