mathlib

93a0ff0d - Add computable inverses alongside surjectivity