Commit 2025-01-31 09:33 c7a5e3b7

View on Github →

chore(Submonoid/Membership): don't import MonoidWithZero (#20748) See #10327 for the new copyright header

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Submonoid/Membership.lean

deleted theorem MulMemClass.mul_left_mem_add_closure

deleted theorem MulMemClass.mul_mem_add_closure

deleted theorem MulMemClass.mul_right_mem_add_closure

deleted def Submonoid.isPrimal

Modified Mathlib/Algebra/Group/Submonoid/Pointwise.lean

Modified Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

Created Mathlib/Algebra/GroupWithZero/Submonoid.lean

added def Submonoid.isPrimal

Created Mathlib/Algebra/Ring/Submonoid.lean

added theorem MulMemClass.mul_left_mem_add_closure

added theorem MulMemClass.mul_mem_add_closure

added theorem MulMemClass.mul_right_mem_add_closure

Modified Mathlib/GroupTheory/MonoidLocalization/Away.lean

Modified Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean