basic): avoid `λ ⟨a, b⟩` in some defs, add `simp` lemmas (#3530)

Commit

5 years ago

chore(data/equiv/basic): avoid `λ ⟨a, b⟩` in some defs, add `simp` lemmas (#3530)

Author

urkud

Parents