Commit 2023-04-06 10:44 332ff816

View on Github →

feat: port RingTheory.QuotientNilpotent (#3293)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/QuotientNilpotent.lean

added theorem Ideal.IsNilpotent.induction_on

added theorem Ideal.isRadical_iff_quotient_reduced

added theorem IsNilpotent.isUnit_quotient_mk_iff