Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-29 11:45 1b3347df

View on Github →

feat(algebra/,data/real/): add some inequalities about canonically_ordered_comm_semirings (#1746) Use them for nnreal and ennreal.

Estimated changes

Modified src/algebra/group_power.lean

added theorem canonically_ordered_semiring.one_le_pow_of_one_le

added theorem canonically_ordered_semiring.pow_le_one

added theorem canonically_ordered_semiring.pow_le_pow_of_le_left

added theorem canonically_ordered_semiring.pow_pos

Modified src/algebra/ordered_ring.lean

modified theorem canonically_ordered_semiring.mul_le_mul

added theorem canonically_ordered_semiring.mul_pos

added theorem canonically_ordered_semiring.zero_lt_one

Modified src/data/real/ennreal.lean