Commit 2024-10-25 15:28 7f067051

View on Github →

feat: add pow_sub_one_dvd_differentIdeal (#18228) From flt-regular.

Estimated changes

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

added theorem pow_sub_one_dvd_differentIdeal

added theorem pow_sub_one_dvd_differentIdeal_aux

Modified Mathlib/RingTheory/Trace/Basic.lean

added theorem Algebra.trace_isNilpotent_of_isNilpotent