mathlib
a15ae9c5 - chore(measure_theory/measurable_space): add simps config for `measurable_equiv` (#9315)

Commit

4 years ago

chore(measure_theory/measurable_space): add simps config for `measurable_equiv` (#9315) Also add `@[ext]` lemma and some standard `equiv` lemmas.

Author

urkud

Parents