Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-15 09:53 03a250a4

View on Github →

chore(data/sym/sym2): Better lemma names (#10801) Renames

  • mk_has_mem to mk_mem_left
  • mk_has_mem_right to mk_mem_right. Just doesn't follow the convention.
  • mem_other to other in lemma names. The mem is confusing and is only part of the fully qualified name for dot notation to work.
  • sym2.elems_iff_eq to mem_and_mem_iff. elems is never used elsewhere. Could also be mem_mem_iff.
  • is_diag_iff_eq to mk_is_diag_iff. The form of the argument was ambiguous. Adding mk solves it.

Estimated changes

modified theorem sym2.coe_lift_symm_apply
modified theorem sym2.diag_is_diag
deleted theorem sym2.elems_iff_eq
modified theorem sym2.from_rel_proj_prop
modified theorem sym2.from_rel_prop
deleted theorem sym2.is_diag_iff_eq
modified def sym2.lift
modified theorem sym2.lift_mk
modified theorem sym2.map.injective
modified def sym2.map
modified theorem sym2.map_comp
modified theorem sym2.map_map
modified theorem sym2.map_pair_eq
added theorem sym2.mem_and_mem_iff
added theorem sym2.mem_mk_left
added theorem sym2.mem_mk_right
deleted theorem sym2.mem_other_mem'
deleted theorem sym2.mem_other_mem
deleted theorem sym2.mem_other_ne
deleted theorem sym2.mem_other_spec'
deleted theorem sym2.mem_other_spec
deleted theorem sym2.mk_has_mem
deleted theorem sym2.mk_has_mem_right
added theorem sym2.mk_is_diag_iff
modified theorem sym2.other_invol'
modified theorem sym2.other_invol
added theorem sym2.other_mem'
added theorem sym2.other_mem
added theorem sym2.other_ne
added theorem sym2.other_spec'
added theorem sym2.other_spec
modified theorem sym2.rel_bool_spec
modified def sym2.sym2_equiv_sym'
deleted theorem sym2.sym2_ext