mathlib3
cac4e196 - feat(set_theory/ordinal_arithmetic): Proved characterization of `log` (#11192)

Commit

4 years ago

feat(set_theory/ordinal_arithmetic): Proved characterization of `log` (#11192) As well as a few simple missing lemmas.

Author

vihdzp

Parents