Commit 2025-10-01 10:39 1b877935

View on Github →

feat(RingTheory): units are exactly non-zerodivisors in noncommutative Artinian rings (#28887)

Estimated changes

Modified Mathlib/RingTheory/Artinian/Algebra.lean

Modified Mathlib/RingTheory/Artinian/Module.lean

added theorem IsArtinianRing.isUnitSubmonoid_eq

added theorem IsArtinianRing.isUnitSubmonoid_eq_nonZeroDivisorsRight

added theorem IsArtinianRing.isUnitSubmonoid_eq_of_mulOpposite

added theorem IsArtinianRing.isUnit_iff_isLeftRegular

added theorem IsArtinianRing.isUnit_iff_isRegular

added theorem IsArtinianRing.isUnit_iff_isRegular_of_mulOpposite

added theorem IsArtinianRing.isUnit_iff_isRightRegular

added theorem IsArtinianRing.isUnit_iff_mem_nonZeroDivisors

added theorem IsArtinianRing.isUnit_iff_mem_nonZeroDivisors_of_mulOpposite

added theorem IsArtinianRing.isUnit_of_mem_nonZeroDivisors

added theorem IsArtinianRing.isUnit_of_mem_nonZeroDivisors_of_mulOpposite

added theorem IsArtinianRing.nonZeroDivisorsLeft_eq_isUnitSubmonoid

Modified Mathlib/RingTheory/Artinian/Ring.lean

deleted theorem IsArtinianRing.isUnit_iff_mem_nonZeroDivisors

deleted theorem IsArtinianRing.isUnit_of_mem_nonZeroDivisors

deleted theorem IsArtinianRing.isUnit_submonoid_eq

Modified Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean

modified theorem Algebra.finite_adjoin_simple_of_isIntegral