mul_cast_floor_div_cancel_of_pos

Mathlib.Algebra.Order.Floor.Ring

URI: https://scilib.ai/kg/mathlib#Int.mul_cast_floor_div_cancel_of_pos

English

For n ∈ ℤ, n > 0, and a ∈ k: ⌊n · a⌋ / n = ⌊a⌋.

Русский

Для n ∈ ℤ, n > 0 и a ∈ k: ⌊n · a⌋ / n = ⌊a⌋.

LaTeX

$$$$\forall n \in \mathbb{Z},\ n > 0:\ \left\lfloor n \cdot a \right\rfloor / n = \left\lfloor a \right\rfloor.$$$$

Lean4

theorem mul_cast_floor_div_cancel_of_pos {n : ℤ} (hn : 0 < n) (a : k) : ⌊a * n⌋ / n = ⌊a⌋ := by
  rw [mul_comm, cast_mul_floor_div_cancel_of_pos hn]

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

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

Разделы

Аффилиация

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