Commit 2026-09-11 04:13 63ed4eba

View on Github →

chore(Algebra/Regular/SMul): split out GroupWithZero (#43679) The new module name Mathlib.Algebra.GroupWithZero.Action.Regular matches the existing Mathlib.Algebra.GroupWithZero.Regular and uses an existing folder.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/GroupWithZero/Action/Regular.lean

added theorem IsSMulRegular.not_zero

added theorem IsSMulRegular.not_zero_iff

added theorem IsSMulRegular.zero

added theorem IsSMulRegular.zero_iff_subsingleton

added theorem isSMulRegular_iff_right_eq_zero_of_smul

Modified Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

Modified Mathlib/Algebra/Regular/Pi.lean

Modified Mathlib/Algebra/Regular/SMul.lean

deleted theorem IsSMulRegular.not_zero

deleted theorem IsSMulRegular.not_zero_iff

deleted theorem IsSMulRegular.zero

deleted theorem IsSMulRegular.zero_iff_subsingleton

deleted theorem isSMulRegular_iff_right_eq_zero_of_smul

Modified Mathlib/AlgebraicGeometry/Modules/Tilde.lean

Modified Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean

Modified Mathlib/RingTheory/Regular/Free.lean

Modified Mathlib/RingTheory/Regular/IsSMulRegular.lean

Modified Mathlib/Topology/Instances/AddCircle/Defs.lean