coe_inj

Mathlib.Tactic.PNatToNat

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.PNatToNat.coe_inj

Lean4

@[pnat_to_nat_coe]
theorem coe_inj (m n : PNat) : m = n ↔ (m : ℕ) = (n : ℕ) := by simp

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

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

Разделы

Аффилиация

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