Commit 2021-10-23 08:22 294ce353

View on Github →

fix(algebra/module/submodule): fix incorrectly generalized arguments to smul_mem_iff' and smul_of_tower_mem (#9851) These put unnecessary requirements on S.

Estimated changes

Modified src/algebra/module/submodule.lean

modified theorem submodule.coe_smul_of_tower

modified theorem submodule.smul_mem_iff'

modified theorem submodule.smul_of_tower_mem

Modified src/group_theory/group_action/sub_mul_action.lean

modified theorem sub_mul_action.smul_mem_iff'

modified theorem sub_mul_action.smul_of_tower_mem

Modified src/topology/algebra/module.lean