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