mathlib3

9c98e1c1 - finish proof of dirichlet_inv_is_inv