Mathlib v3 is deprecated. Go to Mathlib v4

Inductive tactic.positivity.order_rel

Modification history

2022-10-05 09:33

src/tactic/positivity.lean

feat(tactic/positivity): Handle `a ≠ 0` assumptions (#16529) …

Added tactic.positivity.order_rel View on Github →