mathlib3
a8f2bab2 - chore(set_theory/cardinal): use notation `#`, add notation `ω` (#9217)

Commit

4 years ago

chore(set_theory/cardinal): use notation `#`, add notation `ω` (#9217) The only API change: rename `cardinal.eq_congr` to `cardinal.mk_congr`.

Author

urkud

Parents