Commit 2024-04-02 23:42 5f4e6d8b

View on Github →

feat: pointwise scalar multiplication is monotone (#11809) Everywhere we have a smul_mem_pointwise_smul lemma, I've added this result.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Subalgebra/Pointwise.lean

Modified Mathlib/Algebra/Module/Submodule/Pointwise.lean

modified theorem Submodule.set_smul_mono_right

Created Mathlib/Algebra/Order/Group/Action.lean

added theorem smul_iInf_le

added theorem smul_inf_le

added theorem smul_le_smul_left

added theorem smul_mono_right

added theorem smul_strictMono_right

Modified Mathlib/GroupTheory/Subgroup/Pointwise.lean

Modified Mathlib/GroupTheory/Submonoid/Pointwise.lean

Modified Mathlib/RingTheory/Filtration.lean

Modified Mathlib/RingTheory/Ideal/Operations.lean

deleted theorem Submodule.smul_iInf_le

deleted theorem Submodule.smul_inf_le

deleted theorem Submodule.smul_mono_right

Modified Mathlib/RingTheory/Subring/Pointwise.lean

Modified Mathlib/RingTheory/Subsemiring/Pointwise.lean

Modified Mathlib/RingTheory/Valuation/ValuationSubring.lean