Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-30 07:56 da66bb81

View on Github →

feat(*): preparations for roots of unity (#4322)

Estimated changes

Modified src/algebra/group_power/lemmas.lean

added theorem is_unit_of_pow_eq_one

Modified src/data/int/gcd.lean

added theorem pow_gcd_eq_one

Modified src/data/polynomial/ring_division.lean

modified theorem polynomial.card_nth_roots

modified theorem polynomial.mem_nth_roots

modified def polynomial.nth_roots

added theorem polynomial.nth_roots_zero

Modified src/group_theory/order_of_element.lean