Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-19 16:03 bfe73188

View on Github →
  • feat(tactic/mono): new mono and ac_mono tactics (#85)
  • feat(tactic/mono): new mono and ac_mono tactics
  • docs(tactic/mono): improve explanation, examples and syntax
  • feat(tactic/mono): cache the list of mono lemma to facilitate matching
  • fix(tactic/mono): fix conflict with has_lt
  • update mathlib
  • move lemmas from ordered ring to monotonicity
  • rename monotonic attribute to mono
  • address PR comments
  • fix build

Estimated changes

added theorem abs_le_abs
modified theorem option.is_none_iff_eq_none
added theorem option.not_is_some
added theorem imp_imp_imp
modified theorem with_bot.some_lt_some
added theorem mul_mono_nonneg
added theorem mul_mono_nonpos
added def P
added theorem P_mono
added def Q
added theorem Q_mono
added theorem bar_bar''
added theorem bar_bar'
added theorem bar_bar
added def list.le'
added theorem list.le_refl
added theorem list.le_trans
added theorem list_le_mono_left
added theorem list_le_mono_right