feat(data/equiv/local_equiv): define local equivalences (#1359) · leanprover-community/mathlib@6292825 · GitHub

Commit

feat(data/equiv/local_equiv): define local equivalences (#1359)

Browse files

* feat(data/equiv/local_equiv): define local equivalences

* add doc

* add extensionality attribute

* sanity_check

Loading branch information

sgouezel authored and mergify[bot] committed Sep 5, 2019

1 parent 79a1f84 commit 6292825