Commit 2024-12-11 07:05 097f9d2d
View on Github →chore(SetTheory/Ordinal/Arithmetic): move add_mul_limit (#19805)
This has nothing to do with ω and can be moved much earlier in the file.
We also private the auxiliary lemma add_mul_limit_aux.
chore(SetTheory/Ordinal/Arithmetic): move add_mul_limit (#19805)
This has nothing to do with ω and can be moved much earlier in the file.
We also private the auxiliary lemma add_mul_limit_aux.