Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-12-07 00:39 5f642d83

View on Github →

refactor(*): remove local simp AC lemmas Using local simp lemmas everywhere for mul_assoc and friends defeats the purpose of the change in core. Now theorems are proven with only the AC lemmas actually used in the proof.

Estimated changes

added theorem div_eq_inv_mul
added theorem le_max_left_iff_true
added theorem le_max_right_iff_true
added theorem max.left_comm
added theorem max.right_comm
added theorem min_right_comm
modified theorem le_of_not_lt
added theorem le_or_lt
added theorem lt_or_le
modified theorem not_le
modified theorem not_lt
added theorem ennreal.le_def
added theorem nonneg_antisymm
modified theorem uniform_embedding_mul_rat
modified theorem is_closed_iff_nhds
modified theorem is_open_iff_mem_nhds
modified theorem is_open_iff_nhds
added theorem mem_interior
modified theorem finset.insert_eq
modified theorem finset.insert_subset
modified theorem finset.insert_union
modified theorem finset.inter_assoc
modified theorem finset.inter_comm
modified theorem finset.inter_left_comm
modified theorem finset.inter_right_comm
modified theorem finset.union_assoc
modified theorem finset.union_comm
modified theorem finset.union_insert
modified theorem finset.union_left_comm
deleted theorem le_max_left_iff_true
deleted theorem le_max_right_iff_true
deleted theorem max.left_comm
deleted theorem max.right_comm
deleted theorem min_right_comm
deleted theorem not_le_iff
deleted theorem not_lt_iff