Commit 2026-09-30 01:41 380f2aaf

chore: extract lemma from Cardinal.mul_self (#44006) We extract the main lemma from the proof of Cardinal.mul_self: if α can be embedded in a well-order such that any initial segment has cardinal less than c, then α has cardinal at most c. Besides shortening the proof, this avoids the use of unbundled relations; the long-term goal is to move away from them in the Ordinal API entirely.