natCast_injective

Mathlib.Data.Rat.Defs

URI: https://scilib.ai/kg/mathlib#Rat.natCast_injective

English

The natural numbers embed into the rationals and this embedding is injective.

Русский

Естественное вложение ℕ в ℚ инъективно.

LaTeX

$$$ \forall {n m : \mathbb{N}}, (n : \mathbb{Q}) = (m : \mathbb{Q}) \rightarrow n = m $$$

Lean4

theorem natCast_injective : Injective (Nat.cast : ℕ → ℚ) :=
  intCast_injective.comp fun _ _ ↦ Int.natCast_inj.1

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

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

Разделы

Аффилиация

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