Commit 2023-12-06 11:04 07e59b70

View on Github →

chore: Move RingTheory/NonZeroDivisors under Algebra instead. (#8685)

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/RingTheory/NonZeroDivisors.lean to Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

added theorem coe_nonZeroDivisorsLeft_eq

added theorem coe_nonZeroDivisorsRight_eq

added theorem mem_nonZeroDivisorsLeft_iff

added theorem mem_nonZeroDivisorsRight_iff

added def nonZeroDivisorsLeft

added theorem nonZeroDivisorsLeft_eq_right

added def nonZeroDivisorsRight

Deleted Mathlib/GroupTheory/Submonoid/ZeroDivisors.lean

deleted theorem coe_nonZeroDivisorsLeft_eq

deleted theorem coe_nonZeroDivisorsRight_eq

deleted theorem mem_nonZeroDivisorsLeft_iff

deleted theorem mem_nonZeroDivisorsRight_iff

deleted def nonZeroDivisorsLeft

deleted theorem nonZeroDivisorsLeft_eq_right

deleted def nonZeroDivisorsRight

Modified Mathlib/LinearAlgebra/SesquilinearForm.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

Modified Mathlib/RingTheory/Localization/Basic.lean

Modified Mathlib/RingTheory/Localization/Integral.lean

Modified Mathlib/RingTheory/Nilpotent.lean

Modified Mathlib/RingTheory/OreLocalization/Basic.lean

Modified Mathlib/RingTheory/Polynomial/ScaleRoots.lean