fract_mul_natCast — Mathlib

English

For any a ∈ R and natural b, there exists z ∈ ℤ such that fract(a) · b − fract(a · b) = z.

Русский

Для любого a ∈ R и натурального b существует z ∈ ℤ такое, что fract(a)·b − fract(a·b) = z.

LaTeX

$$$\\\\exists z \\\\in \\\\mathbb{Z}, \\\\operatorname{fract}(a) \\\\cdot b - \\\\operatorname{fract}(a b) = z$$$

Lean4

theorem fract_mul_natCast (a : R) (b : ℕ) : ∃ z : ℤ, fract a * b - fract (a * b) = z := by
  induction b with
  | zero => use 0; simp
  | succ c hc =>
    rcases hc with ⟨z, hz⟩
    rw [Nat.cast_add, mul_add, mul_add, Nat.cast_one, mul_one, mul_one]
    rcases fract_add (a * c) a with ⟨y, hy⟩
    use z - y
    rw [Int.cast_sub, ← hz, ← hy]
    abel

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