cast_mul_floor_div_cancel_of_pos

Mathlib.Algebra.Order.Floor.Ring

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

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

Lean4

theorem cast_mul_floor_div_cancel_of_pos {n : ℤ} (hn : 0 < n) (a : k) : ⌊n * a⌋ / n = ⌊a⌋ := by
  simpa [hn.ne'] using (floor_div_cast_of_nonneg hn.le (↑n * a)).symm

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

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

Разделы

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

Аффилиация

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