Commit 2022-05-23 20:34 3f0a2bb4
View on Github →feat(set_theory/cardinal/basic): Inline instances (#14130) We inline some instances, thus avoiding redundant lemmas. We also clean up the code somewhat.
feat(set_theory/cardinal/basic): Inline instances (#14130) We inline some instances, thus avoiding redundant lemmas. We also clean up the code somewhat.