mathlib

d90f70da - remove set k statement from proof of dirichlet_inv_is_inv