mul_natCast_floor_div_cancel

Mathlib.Algebra.Order.Floor.Ring

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

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{N},\ n \neq 0:\ \left\lfloor n \cdot a \right\rfloor / n = \left\lfloor a \right\rfloor.$$$$

Lean4

theorem mul_natCast_floor_div_cancel {n : ℕ} (hn : n ≠ 0) {a : k} : ⌊a * n⌋ / n = ⌊a⌋ := by
  rw [mul_comm, natCast_mul_floor_div_cancel hn]

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

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

Разделы

Аффилиация

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