Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-22 16:25 3dc8592b

View on Github →

feat(tactic/positivity): Extension for coe (#16141) Add:

  • a case in the main positivity tactic to show that 0 ≤ a in a canonically_ordered_add_monoid
  • positivity_coe, an extension to positivity, to turn 0 ≤ a/0 < a into 0 ≤ ↑a/0 < ↑a when a is of type ℕ, ℤ, ℚ.

Estimated changes

modified theorem ennreal.coe_nonneg
added theorem ereal.coe_ennreal_pos
modified theorem ereal.coe_ennreal_top
modified theorem ereal.coe_ennreal_zero
modified theorem ereal.coe_zero
added theorem hyperreal.coe_nonneg
modified theorem hyperreal.coe_pos