Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-05 17:02 03fda911

View on Github →

refactor(algebra/group_power/lemmas): assume n ≠ 0 instead of 0 < n (#17323) Also rename is_unit_pos_pow_iff to is_unit_pow_iff.

Estimated changes

Modified src/algebra/associated.lean

Modified src/algebra/group_power/lemmas.lean

modified def invertible_of_pow_eq_one

modified theorem is_unit_of_pow_eq_one

deleted theorem is_unit_pos_pow_iff

added theorem is_unit_pow_iff

Modified src/algebra/is_prime_pow.lean

Modified src/data/int/gcd.lean

Modified src/data/polynomial/unit_trinomial.lean

Modified src/field_theory/abel_ruffini.lean

Modified src/linear_algebra/matrix/zpow.lean

Modified src/ring_theory/roots_of_unity.lean