floor_div_cast_of_nonneg — Mathlib

English

For k a field with floor and a ∈ k, and n ∈ ℤ with n ≥ 0, ⌊a / n⌋ = ⌊a⌋ / n.

Русский

Для поля k с функцией floor, a ∈ k и n ∈ ℤ с n ≥ 0, выполняется ⌊a/n⌋ = ⌊a⌋/n.

LaTeX

$$$$\forall k \text{ with floor},\ a \in k,\ n \in \mathbb{Z},\ n \ge 0:\ \left\lfloor \frac{a}{n} \right\rfloor = \frac{\lfloor a \rfloor}{n}.$$$$

Lean4

theorem floor_div_cast_of_nonneg {n : ℤ} (hn : 0 ≤ n) (a : k) : ⌊a / n⌋ = ⌊a⌋ / n :=
  by
  obtain rfl | hn := hn.eq_or_lt
  · simp
  refine eq_of_forall_le_iff fun m ↦ ?_
  rw [Int.le_ediv_iff_mul_le hn, le_floor, le_floor, le_div_iff₀ (by positivity), cast_mul]

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