N_less_than_M_to_the_N
Provedalgebraproofwiki
For all positive integers m > 1 and n > 0: n < m^n.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem N_less_than_M_to_the_N (m n : ℕ) (hm : 1 < m) (hn : 0 < n) : n < m ^ n := by sorry
Source