instRepr

Mathlib.Data.Nat.Prime.Defs

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

English

There is a canonical representation for Nat.Primes by their underlying natural number.

Русский

Существует каноническое представление Nat.Primes через их натуральное значение.

LaTeX

$$$\\text{Repr}(\\mathrm{Nat.Primes})$ определяется отображением $p \\mapsto \\mathrm{repr}(p.\\mathrm{val})$.$$

Lean4

instance : Repr Nat.Primes :=
  ⟨fun p _ => repr p.val⟩

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

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

Разделы

Аффилиация

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