Commit 2024-10-24 16:27 62a047f8

View on Github →

feat: SMul instance for AddSubmonoid and lemmas (#18096)

  • Introduce a SMul instance for two AddSubmonoids and provide lemmas
  • Introduce a Mul instance for AddSubgroup
  • Prove lemmas for the existing Mul instance on AddSubmonoid, which are generalized from corresponding Submodule lemmas

Estimated changes

added theorem AddSubmonoid.iSup_mul
added theorem AddSubmonoid.mul_iSup
modified theorem AddSubmonoid.mul_le_mul
modified theorem AddSubmonoid.mul_subset_mul
added theorem AddSubmonoid.mul_sup
added theorem AddSubmonoid.smul_le
added theorem AddSubmonoid.sup_mul