natCast_floor_eq_intCast_floor — Mathlib

English

If a ≥ 0, then the floor of a, viewed as a member of the ring, equals the floor of a: (⌊a⌋_+ : R) = ⌊a⌋.

Русский

Если a ≥ 0, то пол(a), когда он трактуется как элемент кольца, равен floor(a): (⌊a⌋_+ : R) = ⌊a⌋.

LaTeX

$$$$ 0 \le a \Rightarrow (\lfloor a \rfloor_+ : R) = \lfloor a \rfloor $$$$

Lean4

theorem natCast_floor_eq_intCast_floor (ha : 0 ≤ a) : (⌊a⌋₊ : R) = ⌊a⌋ := by
  rw [← Int.natCast_floor_eq_floor ha, Int.cast_natCast]

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