mathlib
7e3e8834 - chore(data/equiv): add docstrings (#7704)

Commit

4 years ago

chore(data/equiv): add docstrings (#7704) - add module docstrings - add def docstrings - rename `decode2` to `decode₂` - squash some simps

Author

YaelDillies

Parents