mul_cast_floor_div_cancel

Mathlib.Algebra.Order.Floor.Semifield

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

English

Same as above with the factors reversed: ⌊a·n⌋_+ / n = ⌊a⌋_+.

Русский

То же самое, что и выше, но с перемножением слева: ⌊a·n⌋_+ / n = ⌊a⌋_+.

LaTeX

$$$$ \left\lfloor a \cdot n \right\rfloor_+ / n = \left\lfloor a \right\rfloor_+ $$$$

Lean4

theorem mul_cast_floor_div_cancel {n : ℕ} (hn : n ≠ 0) (a : K) : ⌊a * n⌋₊ / n = ⌊a⌋₊ := by
  rw [mul_comm, cast_mul_floor_div_cancel hn]

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

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

Разделы

Аффилиация

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