Commit 2024-12-23 23:12 2a4e3ed8

View on Github →

feat: 0 < n ^ n for all n : ℕ (#20059) From GrowthInGroups (LeanCamCombi)

Estimated changes

Modified Mathlib/Data/Nat/Defs.lean

added theorem Nat.pow_self_mul_pow_self_le

added theorem Nat.pow_self_pos