Junyan Xu

icon indicating an email [email protected]

icon location Heidelberg / Shenzhen icon location PhD in Math, working on Lean's mathlib4 and formalization of FLT. Interested in autoformalization and AI for mathematics.

Results 172 comments of Junyan Xu

feat: SuccOrder and recursion principle on well-ordered type

cc @digama0, the [author](https://github.com/leanprover-community/mathlib/commit/7726a92f) of `ordinal.limit_rec_on`.

feat: SuccOrder and recursion principle on well-ordered type

Thanks for the review and delegation!