mathlib
e9a1e2b3 - refactor(data/pequiv): simpler proof of `pequiv.of_set_univ` (#5907)

Commit

4 years ago

refactor(data/pequiv): simpler proof of `pequiv.of_set_univ` (#5907) 17X smaller proof co-authors: `lean-gptf`, Stanislas Polu

Author

Jesse Michael Han

Parents