Commit 2026-05-18 12:33 3076fd7d

View on Github →

chore: review Cardinal.ord API (#35865) This PR does the following:

  • Mark Cardinal.ord as no expose.
  • Prove the defining property gciOrdCard earlier.
  • Deprecate the unused ord.orderEmbedding (it simply restates that the function is strictly monotonic).
  • Rename ord_nat → ord_natCast.

Estimated changes

modified theorem Cardinal.gc_ord_card
modified theorem Cardinal.mk_toType
modified theorem Cardinal.ord_inj
modified theorem Cardinal.ord_injective
modified theorem Cardinal.ord_le
deleted theorem Cardinal.ord_nat
added theorem Cardinal.ord_natCast
modified theorem Cardinal.ord_one