Commit 2021-12-15 09:53 03a250a4
View on Github →chore(data/sym/sym2): Better lemma names (#10801) Renames
mk_has_mem
tomk_mem_left
mk_has_mem_right
tomk_mem_right
. Just doesn't follow the convention.mem_other
toother
in lemma names. Themem
is confusing and is only part of the fully qualified name for dot notation to work.sym2.elems_iff_eq
tomem_and_mem_iff
.elems
is never used elsewhere. Could also bemem_mem_iff
.is_diag_iff_eq
tomk_is_diag_iff
. The form of the argument was ambiguous. Addingmk
solves it.