intCast_injOn_Ico — Mathlib

English

The map Int.cast is injective on the interval Ico(0,p) (i.e., {0,...,p-1}).

Русский

Карта Int.cast инъективна на промежутке Ico(0,p) (то есть на {0,...,p-1}).

LaTeX

$$[IsRightCancelAdd R] ⇒ InjOn (Int.cast : ℤ → R) (Ico 0 p)$$

Lean4

theorem intCast_injOn_Ico [IsRightCancelAdd R] : InjOn (Int.cast : ℤ → R) (Ico 0 p) :=
  by
  rintro a ⟨ha₀, ha⟩ b ⟨hb₀, hb⟩ hab
  lift a to ℕ using ha₀
  lift b to ℕ using hb₀
  norm_cast at *
  exact natCast_injOn_Iio _ _ ha hb hab

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