Commit 2024-12-04 12:33 a38db992

View on Github →

refactor: generalize SMul (Ideal R) (Submodule R M) to SMul (Submodule R A) (Submodule R M) (#18419) and redefine Mul (Submodule R A) (Submodule R A) using the latter.

Estimated changes

Modified Mathlib/Algebra/Algebra/Operations.lean

added theorem Submodule.bot_smul

added theorem Submodule.coe_set_smul

added theorem Submodule.iSup_smul

added theorem Submodule.smul_bot

added theorem Submodule.smul_iSup

added theorem Submodule.smul_induction_on'

added theorem Submodule.smul_induction_on

added theorem Submodule.smul_le

added theorem Submodule.smul_mem_smul

added theorem Submodule.smul_mono

added theorem Submodule.smul_mono_left

added theorem Submodule.smul_subset_smul

added theorem Submodule.smul_sup

added theorem Submodule.smul_toAddSubmonoid

added theorem Submodule.sup_smul

Modified Mathlib/RingTheory/Ideal/Operations.lean

deleted theorem Submodule.bot_smul

deleted theorem Submodule.coe_set_smul

deleted theorem Submodule.smul_bot

deleted theorem Submodule.smul_iSup

deleted theorem Submodule.smul_induction_on'

deleted theorem Submodule.smul_induction_on

deleted theorem Submodule.smul_le

deleted theorem Submodule.smul_mem_smul

deleted theorem Submodule.smul_mono

deleted theorem Submodule.smul_mono_left

deleted theorem Submodule.smul_sup

deleted theorem Submodule.smul_toAddSubmonoid

deleted theorem Submodule.sup_smul