ceil_intCast

Mathlib.Algebra.Order.Floor.Semiring

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

← MathLib Explorer

English

For any z ∈ ℤ, ⌈z : R⌉₊ = z.toNat.

Русский

Пусть z ∈ ℤ. Тогда ⌈z : R⌉₊ = z.toNat.

LaTeX

$$$ \lceil z \rceil_{+} = z.{\\mathrm{toNat}} $$$

Lean4

@[simp]
theorem ceil_intCast {R : Type*} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] [FloorSemiring R] (z : ℤ) :
    ⌈(z : R)⌉₊ = z.toNat :=
  eq_of_forall_ge_iff fun a => by
    simp only [ceil_le, Int.toNat_le]
    norm_cast

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

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

Разделы

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

Аффилиация

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