Commit 2023-11-02 11:46 3a5265f9

View on Github →

feat: bijective_iff_map_univ_eq_univ (#7120) For functions on finite sets, they are bijections iff they map universes into universes.

Estimated changes