Theorem Algebra.trace_isNilpotent_of_isNilpotent

Modification history

2024-10-25 15:28
Mathlib/RingTheory/Trace/Basic.lean
feat: add pow_sub_one_dvd_differentIdeal (#18228) …
Added Algebra.trace_isNilpotent_of_isNilpotentView on Github →