Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-15 15:53 c0c673ab

View on Github →

feat(data/equiv,logic/embedding): add can_lift instances (#12049)

Estimated changes

Modified src/data/equiv/basic.lean

modified theorem equiv.of_bijective_apply_symm_apply

modified theorem equiv.of_bijective_symm_apply_apply

Modified src/logic/embedding.lean