mathlib
03a250a4 - chore(data/sym/sym2): Better lemma names (#10801)

Commit
4 years ago
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.
Author
Parents
Loading