Commit 2023-09-26 09:02 bf1ceb82

View on Github →

feat: lemmas about divisibility, mostly related to nilpotency (#7355)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Multiset/Basic.lean

Modified Mathlib/Algebra/BigOperators/Ring.lean

modified theorem Finset.dvd_sum

Modified Mathlib/Algebra/EuclideanDomain/Basic.lean

Modified Mathlib/Algebra/GroupPower/Ring.lean

added theorem neg_pow'

Modified Mathlib/Algebra/Order/Ring/Abs.lean

Renamed Mathlib/Algebra/Ring/Divisibility.lean to Mathlib/Algebra/Ring/Divisibility/Basic.lean

Created Mathlib/Algebra/Ring/Divisibility/Lemmas.lean

added theorem Commute.add_pow_dvd_pow_of_pow_eq_zero_left

added theorem Commute.add_pow_dvd_pow_of_pow_eq_zero_right

added theorem Commute.pow_dvd_add_pow_of_pow_eq_zero_left

added theorem Commute.pow_dvd_add_pow_of_pow_eq_zero_right

added theorem Commute.pow_dvd_pow_of_add_pow_eq_zero

added theorem Commute.pow_dvd_pow_of_sub_pow_eq_zero

added theorem Commute.pow_dvd_sub_pow_of_pow_eq_zero_left

added theorem Commute.pow_dvd_sub_pow_of_pow_eq_zero_right

added theorem dvd_nsmul_of_dvd

added theorem dvd_smul_of_dvd

added theorem dvd_zsmul_of_dvd

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

Modified Mathlib/Data/List/BigOperators/Lemmas.lean

modified theorem List.dvd_sum

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

Modified Mathlib/RingTheory/Coprime/Basic.lean