fract_div_mul_self_add_zsmul_eq — Mathlib

English

For k a field, a ≠ 0, we have fract(b/a)·a + floor(b/a)·a = b.

Русский

Пусть k — поле, a ≠ 0; тогда fract(b/a)·a + floor(b/a)·a = b.

LaTeX

$$$\\\\operatorname{fract}(\\\\frac{b}{a}) \\\\cdot a + \\\\lfloor\\\\frac{b}{a}\\\\rfloor \\\\cdot a = b$$$

Lean4

theorem fract_div_mul_self_add_zsmul_eq (a b : k) (ha : a ≠ 0) : fract (b / a) * a + ⌊b / a⌋ • a = b := by
  rw [zsmul_eq_mul, ← add_mul, fract_add_floor, div_mul_cancel₀ b ha]

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