factorial_inj'

Mathlib.Data.Nat.Factorial.Basic

URI: https://scilib.ai/kg/mathlib#Nat.factorial_inj'

← MathLib Explorer

English

For natural numbers m,n, if 1 < n ∨ 1 < m, then n! = m! iff n = m.

Русский

Для естественных чисел m,n, если 1 < n или 1 < m, то n! = m! ↔ n = m.

LaTeX

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

Lean4

theorem factorial_inj' (h : 1 < n ∨ 1 < m) : n ! = m ! ↔ n = m :=
  by
  obtain hn | hm := h
  · exact factorial_inj hn
  · rw [eq_comm, factorial_inj hm, eq_comm]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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