coe_pnat_inj

Mathlib.Data.PNat.Prime

URI: https://scilib.ai/kg/mathlib#Nat.Primes.coe_pnat_inj

English

For p,q ∈ Nat.Primes, the mapping p ↦ p.toPNat is injective.

Русский

Для p,q ∈ Nat.Primes отображение p ↦ p.toPNat инъективно.

LaTeX

$$$\\forall p,q \\in Nat.Primes,\\; p.{\\mathrm{toPNat}} = q.{\\mathrm{toPNat}} \\Rightarrow p = q$$$

Lean4

@[norm_cast]
theorem coe_pnat_inj (p q : Nat.Primes) : (p : ℕ+) = (q : ℕ+) ↔ p = q :=
  coe_pnat_injective.eq_iff

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

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

Разделы

Аффилиация

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