Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-21 17:46 472156f9

View on Github →

feat(tactic/lint): check that left-hand side of all simp lemmas is in simp-normal form (#2017)

  • feat(tactic/lint): check that lhs of simp lemmas are in simp nf
  • fix(topology/metric_space/basic): remove @[simp] from lemmas with {x,y} on the lhs
  • chore(topology/local_homeomorph): remove redundant lemmas from the simp set
  • fix(topology/algebra/module): fix simp-nf lints
  • chore(ring_theory/localization): mark fewer things as simp
  • fix(set_theory/ordinal): put lhs into simp-normal form
  • chore(algebra/big_operators): fix simp lemmas
  • chore(data/set/lattice): remove redundant simp lemmas
  • chore(data/set/basic): remove redundant simp lemma
  • chore(data/zsqrtd/basic): make simp_nf lint happy
  • fix(order/complete_lattice): remove lemmas from simp set
  • chore(order/filter/filter_product): fix linting issues
  • feat(data/mv_polynomial): add simp lemmas about neg
  • fix(data/multiset): fix simp_nf linter issues
  • chore(data/list/sigma): fix simp_nf linter issues
  • fix(data/list/basic): remove redundant and unapplicable simp lemmas
  • fix(measure_theory/set_integral): remove redundant simp lemma
  • fix(measure_theory/l1_space): remove redundant simp lemmas
  • fix(algebra/group_power): remove simp lemmas that are not in nf
  • fix(algebra/field): remove redundant simp lemma
  • chore(data/list/alist): remove simp lemmas
  • fix(data/int/basic): simp-normal form for coercions...
  • fix(data/finset): formulate simp-lemmas for simp-nf
  • fix(data/int/parity): use simp-normal form
  • fix(data/equiv/denumerable): remove redundant simp lemma
  • fix(category_theory/**): fix simp-normal forms
  • fix(set_theory/zfc): put simp lemmas in simp-normal form
  • fix(tactlic/lint): ignore sub_eq_add_neg for simp_nf lint
  • doc(tactic/lint): add simp_nf linter to module doc
  • doc(docs/commands): add simp_nf linter
  • fix(*): put lemmas in simp-normal form

Estimated changes

modified theorem finset.sum_boole_mul
modified theorem finset.sum_mul_boole
deleted theorem units.mk0_inv
modified theorem gpow_of_nat
modified theorem gsmul_of_nat
modified theorem one_div_pow
added theorem ite_mul
modified theorem denumerable.decode_is_some
added theorem finset.inf_singleton'
modified theorem finset.inf_singleton
modified theorem finset.max_singleton
added theorem finset.min_singleton'
modified theorem finset.min_singleton
added theorem finset.sup_singleton'
modified theorem finset.sup_singleton
modified theorem finset.supr_union
modified theorem int.cast_coe_nat'
modified theorem int.cast_of_nat
modified theorem int.mod_two_ne_zero
added theorem int.two_dvd_ne_zero
modified theorem alist.insert_insert_of_ne
modified theorem list.concat_append
modified theorem list.concat_cons
modified theorem list.concat_ne_nil
modified theorem list.concat_nil
modified theorem list.count_concat
modified theorem list.exists_mem_cons_iff
added theorem list.infix_append'
modified theorem list.infix_append
modified theorem list.length_concat
modified theorem list.prefix_concat
modified theorem list.lookup_kinsert
modified theorem list.lookup_kinsert_ne
modified theorem list.mem_keys_kinsert
modified theorem multiset.map_singleton
modified theorem multiset.prod_map_one
modified theorem multiset.sum_map_zero
modified theorem set.nmem_set_of_eq
modified theorem set.subset_preimage_univ
modified theorem set.bInter_empty
modified theorem set.bInter_univ
modified theorem set.bUnion_empty
modified theorem set.bUnion_univ
modified theorem zsqrtd.of_int_im
modified theorem zsqrtd.of_int_re
modified theorem integral_on_zero
modified theorem lattice.infi_emptyset
modified theorem lattice.infi_insert
modified theorem lattice.infi_pair
modified theorem lattice.infi_singleton
modified theorem lattice.infi_union
modified theorem lattice.infi_univ
modified theorem lattice.supr_emptyset
modified theorem lattice.supr_insert
modified theorem lattice.supr_pair
modified theorem lattice.supr_singleton
modified theorem lattice.supr_union
modified theorem lattice.supr_univ
modified theorem localization.coe_is_unit'
modified theorem localization.coe_is_unit
modified theorem localization.coe_mul_mk
modified theorem localization.lift'_mk
modified theorem localization.mk_mul_mk
modified theorem localization.to_units_coe
added theorem Set.eval_mk
modified theorem pSet.resp.eval_val
modified theorem metric.diam_pair
modified theorem metric.diam_triple
added def c
added theorem c_eq_d
added def d
added def f
added theorem f_c
added def h
added theorem h_c
added structure morphism