Commit 2024-01-16 13:08 f6355632

View on Github →

chore: Move Int.pow_right_injective (#9739) This allows more files to not depend on Algebra.GroupPower.Lemmas, which will soon stop existing. Part of #9411

Estimated changes

Modified Mathlib/Algebra/GroupPower/Lemmas.lean

deleted theorem Int.pow_right_injective

Modified Mathlib/Data/Int/Order/Lemmas.lean

added theorem Int.pow_right_injective

Modified Mathlib/GroupTheory/Submonoid/Membership.lean