mathlib

7077b588 - chore(logic/function): move to `logic/function/basic` (#2677)

chore(logic/function): move to `logic/function/basic` (#2677) Also add some docstrings. I'm going to add more `logic.function.*` files with theorems that can't go to `basic` because of imports.