Commit 2026-05-30 11:31 515b1087

refactor(Data/ZMod): move coe_int_isUnit_iff_isCoprime to ZMod.Units (#38340) Move ZMod.coe_int_isUnit_iff_isCoprime from Mathlib.Data.ZMod.Coprime to Mathlib.Data.ZMod.Units, where it more naturally belongs as a statement about units in ZMod. The proof is rewritten to only use tools available in Mathlib.Data.ZMod.Units, avoiding the dependency on Mathlib.Algebra.EuclideanDomain.Int. This is motivated by the desire to use coe_int_isUnit_iff_isCoprime without the overhead of importing Mathlib.Data.ZMod.Coprime (see #38339 for a use case).