mathlib

1000ae8d - doc(*): new documentation requirements (#1229)

doc(*): new documentation requirements (#1229) * feat(docs/contribute/doc): template for documentation * doc(data/padics/padic_norm): new doc style * doc(docs/contribute/code-review): add link to doc requirements * doc(.github/PULL_REQUEST_TEMPLATE): add link to doc requirements * doc(topology/basic): adds new style documentation * feat(tactic/doc_blame): a user command #doc_blame It lists definitions without docstrings in the current file * perf(tactic/doc_blame): filter declarations earlier * doc(contribute/doc): More doc style explanations * doc(data/padics/padic_norm): finish documenting * doc(docs/contribute/docs): more text about documentation requirements * feat(tactic/doc_blame): add option to blame theorems also * doc(cardinal/ordinal): add some documentation add header to cardinal.lean fix some information in topological_spaces.md (but not all) * fix(data/padics): remove leftover exit command * doc(*): update proposed doc style * doc(docs/contribute/doc.md): update doc style guide * feat(docs/references): add mathlib references bibtex * update doc style in times_cont_diff and add to list of examples * fix(docs/contribute/doc): clarify implementation notes * doc(tactic/doc_blame): add header