coeNat

Mathlib.Data.Nat.Prime.Defs

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

English

There is a natural embedding of Nat.Primes into ℕ given by the underlying value.

Русский

Существует естественное вложение Nat.Primes в ℕ через их значение.

LaTeX

$$$\\iota: \\mathrm{Nat.Primes} \\to \\mathbb{N}$ задаётся $\\iota(p) = p.\\mathrm{val}$.$$

Lean4

instance coeNat : Coe Nat.Primes ℕ :=
  ⟨Subtype.val⟩

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

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

Разделы

Аффилиация

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