natCast_injOn_Iio

Mathlib.Algebra.CharP.Basic

URI: https://scilib.ai/kg/mathlib#CharP.natCast_injOn_Iio

English

The map from natural numbers to R via natCast is injective on the interval {0,1,...,p-1}.

Русский

Отображение натуральных чисел в R через natCast инъективно на множестве {0,1,...,p-1}.

LaTeX

$$$ (Set.Iio\ p).InjOn (Nat.cast : \mathbb{N} \to R) $$$

Lean4

theorem natCast_injOn_Iio : (Set.Iio p).InjOn ((↑) : ℕ → R) := fun _a ha _b hb hab ↦
  ((natCast_eq_natCast _ _).1 hab).eq_of_lt_of_lt ha hb

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

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

Разделы

Аффилиация

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