factorial_inj — Mathlib

English

For n > 1, n! = m! iff n = m.

Русский

Для n > 1: n! = m! тогда и только тогда, когда n = m.

LaTeX

$$$\forall {m,n:\mathbb{N}}, 1 < n \rightarrow (n! = m! \iff n = m)$$$

Lean4

theorem factorial_inj (hn : 1 < n) : n ! = m ! ↔ n = m :=
  by
  refine ⟨fun h => ?_, congr_arg _⟩
  obtain hnm | rfl | hnm := lt_trichotomy n m
  · rw [← factorial_lt <| lt_of_succ_lt hn, h] at hnm
    cases lt_irrefl _ hnm
  · rfl
  rw [← one_lt_factorial, h, one_lt_factorial] at hn
  rw [← factorial_lt <| lt_of_succ_lt hn, h] at hnm
  cases lt_irrefl _ hnm

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