Commit 2024-10-28 06:12 95c5f3f5

View on Github →

refactor: generalize AddSubmonoid Mul lemmas to SMul (#18278)

Estimated changes

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

added theorem AddSubmonoid.addSubmonoid_smul_bot

added theorem AddSubmonoid.addSubmonoid_smul_sup

added theorem AddSubmonoid.smul_iSup

added theorem AddSubmonoid.smul_le_smul_left

added theorem AddSubmonoid.smul_le_smul_right

added theorem AddSubmonoid.smul_subset_smul

Modified Mathlib/Algebra/GroupWithZero/Action/Defs.lean

Modified Mathlib/Algebra/Module/Defs.lean