mathlib

b36a458a - feat(set_theory/ordinal/basic): add `gc_ord_card` and `gci_ord_card` (#15152)

feat(set_theory/ordinal/basic): add `gc_ord_card` and `gci_ord_card` (#15152) Define a Galois coinsertion between `cardinal.ord` and `ordinal.card`, then use it to golf some proofs.