coe_eq_one_iff

Mathlib.Data.PNat.Defs

URI: https://scilib.ai/kg/mathlib#PNat.coe_eq_one_iff

English

For any m in PNat, (m : ℕ) = 1 if and only if m = 1.

Русский

Для любого m ∈ ℕ⁺, (m : ℕ) = 1 тогда и только тогда, когда m = 1.

LaTeX

$$$\\forall {m : \mathbb{N}^+}, (m : \mathbb{N}) = 1 \\iff m = 1$$$

Lean4

@[simp, norm_cast]
theorem coe_eq_one_iff {m : ℕ+} : (m : ℕ) = 1 ↔ m = 1 :=
  Subtype.coe_injective.eq_iff' one_coe

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

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

Разделы

Аффилиация

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