floor_natCast — Mathlib

English

For every natural number n, the floor of n embedded in the base ring equals n.

Русский

Для каждого натурального числа n целочисленное округление вниз от n, рассм. как элемент кольца, равно n.

LaTeX

$$$\lfloor (n : R) \rfloor_+ = n$$$

Lean4

@[simp]
theorem floor_natCast (n : ℕ) : ⌊(n : R)⌋₊ = n :=
  eq_of_forall_le_iff fun a => by
    rw [le_floor_iff, Nat.cast_le]
    exact n.cast_nonneg

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