arithmetic): more log lemmas (#15447)

Commit

3 years ago

feat(set_theory/ordinal/arithmetic): more log lemmas (#15447) We prove a bunch of lemmas on the ordinal logarithm that are relevant for Cantor normal forms.

Author

vihdzp

Parents

9137502f

mathlib 5e114a3e - feat(set_theory/ordinal/arithmetic): more log lemmas (#15447)

mathlib
5e114a3e - feat(set_theory/ordinal/arithmetic): more log lemmas (#15447)