mathlib

a13086e5 - simplify proof of dirichlet_inv_is_inv