of_nat_inj — Mathlib

English

For natural numbers m and n, (m : Num) = (n : Num) iff m = n.

Русский

Для натуральных m и n: (m : Num) = (n : Num) тогда и только тогда, когда m = n.

LaTeX

$$$\\forall {m n : \\mathbb{N}}, (m : Num) = (n : Num) \\Leftrightarrow m = n$$$

Lean4

@[norm_cast]
theorem of_nat_inj {m n : ℕ} : (m : Num) = n ↔ m = n :=
  ⟨fun h => Function.LeftInverse.injective to_of_nat h, congr_arg _⟩
    -- The priority should be `high`er than `cast_to_nat`.

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