Theorem Int.pow_right_injective

Modification history

2025-02-20 01:21
Mathlib/Data/Int/Basic.lean
chore(Data/Int): split `Defs` into `Init` and `Basic` (#22009) …
Modified Int.pow_right_injectiveView on Github →
2024-07-08 17:58
Mathlib/Data/Int/Defs.lean
chore(Subring): don't import ordered ring classes for basic things (#14126) …
Modified Int.pow_right_injectiveView on Github →
2024-01-16 13:08
Mathlib/Algebra/GroupPower/Lemmas.lean
chore: Move `Int.pow_right_injective` (#9739) …
Modified Int.pow_right_injectiveView on Github →
2023-01-19 10:36
Mathlib/Algebra/GroupPower/Lemmas.lean
chore: format by line breaks with long lines (#1529) …
Modified Int.pow_right_injectiveView on Github →
2022-12-19 11:23
Mathlib/Algebra/GroupPower/Lemmas.lean
feat port Algebra.GroupPower.Lemmas (#1055) …
Added Int.pow_right_injectiveView on Github →