cast_mul_floor_div_cancel

Mathlib.Algebra.Order.Floor.Semifield

URI: https://scilib.ai/kg/mathlib#Nat.cast_mul_floor_div_cancel

English

For a ∈ K and n ∈ ℕ with n ≠ 0, ⌊n·a⌋_+ / n = ⌊a⌋_+.

Русский

При n ≠ 0 верно: ⌊n·a⌋_+ / n = ⌊a⌋_+.

LaTeX

$$$$ \text{for } n \neq 0:\; \left\lfloor n \cdot a \right\rfloor_+ / n = \left\lfloor a \right\rfloor_+ $$$$

Lean4

theorem cast_mul_floor_div_cancel {n : ℕ} (hn : n ≠ 0) (a : K) : ⌊n * a⌋₊ / n = ⌊a⌋₊ := by
  simpa [hn] using (floor_div_natCast (n * a) n).symm

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

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

Разделы

Аффилиация

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