natCast_mul_floor_div_cancel

Mathlib.Algebra.Order.Floor.Ring

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

← MathLib Explorer

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 natCast_mul_floor_div_cancel {n : ℕ} (hn : n ≠ 0) (a : k) : ⌊n * a⌋ / n = ⌊a⌋ := by
  simpa using cast_mul_floor_div_cancel_of_pos (n := n) (by cutsat) a

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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