Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-26 05:06 9bb99568

View on Github →

feat(data/nat/basic): inequalities (#2801) Adds some simple inequalities about nat.pow.

Estimated changes

added theorem nat.lt_two_pow
added theorem nat.one_le_pow'
added theorem nat.one_le_pow
added theorem nat.one_le_two_pow
added theorem nat.one_lt_pow'
added theorem nat.one_lt_pow
added theorem nat.one_lt_two_pow'
added theorem nat.one_lt_two_pow