mathlib3

088fcb0d - prove that dirichlet_inv_fun terminates