mathlib3

e0ecaa9e - feat(set_theory/ordinal/notation): fast growing hierarchy (#14072)

feat(set_theory/ordinal/notation): fast growing hierarchy (#14072) Adds a definition `onote.fast_growing` which yields elements of the [fast-growing hierarchy](https://en.wikipedia.org/wiki/Fast-growing_hierarchy) up to and including ε₀. Because it is built on `onote` instead of `ordinal`, the definition is fully computable, and you can work out some small elements. For example `fast_growing_ε₀ 2 = 2048` and `fast_growing_ε₀ 3` is... big.