mathlib3

1c927ddf - add lemmas about recursive case of dirichlet_inv_fun