basic): subtype_equiv_psigma (#9688)

Commit

4 years ago

feat(data/equiv/basic): subtype_equiv_psigma (#9688) - [x] depends on: #9687 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author

kim-em

Parents

9da33a89

mathlib dc23dfa1 - feat(data/equiv/basic): subtype_equiv_psigma (#9688)

mathlib
dc23dfa1 - feat(data/equiv/basic): subtype_equiv_psigma (#9688)