coe_nat_inj

Mathlib.Data.Nat.Prime.Defs

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

English

For p, q in Nat.Primes, (p.val) = (q.val) iff p = q.

Русский

Для p, q из Nat.Primes, (p.val) = (q.val) тогда и только тогда, когда p = q.

LaTeX

$$$\\\\forall p,q : \\mathrm{Nat.Primes}, (p.\\\\val) = (q.\\\\val) \\\\Leftrightarrow p = q$$$

Lean4

theorem coe_nat_inj (p q : Nat.Primes) : (p : ℕ) = (q : ℕ) ↔ p = q :=
  Subtype.ext_iff.symm

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

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

Разделы

Аффилиация

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