Mathlib v3 is deprecated. Go to Mathlib v4

Theorem equiv.of_bijective_symm_apply_apply

Modification history

2022-02-15 15:53
src/data/equiv/basic.lean
feat(data/equiv,logic/embedding): add `can_lift` instances (#12049)
Modified equiv.of_bijective_symm_apply_applyView on Github →
2020-12-07 10:37
src/data/equiv/basic.lean
feat(dynamics/circle/rotation_number): translation numbers define a group action up to a semiconjugacy (#5138) …
Added equiv.of_bijective_symm_apply_applyView on Github →