Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-23 00:38 671b1797

View on Github →

refactor(group_theory/subgroup,linear_algebra/basic): put pointwise actions in their own files to match submonoid (#9312)

Estimated changes

Modified src/algebra/algebra/operations.lean

Modified src/algebra/category/Group/limits.lean

Modified src/algebra/direct_sum/basic.lean

Modified src/algebra/direct_sum/ring.lean

Modified src/algebra/group_ring_action.lean

Created src/algebra/module/submodule_pointwise.lean

added theorem submodule.add_eq_sup

added theorem submodule.coe_pointwise_smul

added theorem submodule.pointwise_smul_to_add_subgroup

added theorem submodule.pointwise_smul_to_add_submonoid

added theorem submodule.smul_le_self_of_tower

added theorem submodule.smul_mem_pointwise_smul

added theorem submodule.zero_eq_bot

Modified src/deprecated/subgroup.lean

Modified src/group_theory/archimedean.lean

Modified src/group_theory/coset.lean

Modified src/group_theory/finiteness.lean

Modified src/group_theory/free_group.lean

Modified src/group_theory/general_commutator.lean

Modified src/group_theory/perm/subgroup.lean

Modified src/group_theory/semidirect_product.lean

Renamed src/group_theory/subgroup.lean to src/group_theory/subgroup/basic.lean

deleted theorem add_subgroup.coe_pointwise_smul

deleted theorem add_subgroup.pointwise_smul_to_add_submonoid

deleted theorem add_subgroup.smul_mem_pointwise_smul

deleted theorem subgroup.coe_pointwise_smul

deleted theorem subgroup.pointwise_smul_to_submonoid

deleted theorem subgroup.smul_mem_pointwise_smul

Created src/group_theory/subgroup/pointwise.lean

added theorem add_subgroup.coe_pointwise_smul

added theorem add_subgroup.pointwise_smul_to_add_submonoid

added theorem add_subgroup.smul_mem_pointwise_smul

added theorem subgroup.coe_pointwise_smul

added theorem subgroup.pointwise_smul_to_submonoid

added theorem subgroup.smul_mem_pointwise_smul

Modified src/group_theory/submonoid/pointwise.lean

Modified src/linear_algebra/basic.lean

deleted theorem submodule.add_eq_sup

deleted theorem submodule.coe_pointwise_smul

deleted theorem submodule.lt_add_iff_not_mem

added theorem submodule.lt_sup_iff_not_mem

modified theorem submodule.map_add_le

deleted theorem submodule.pointwise_smul_to_add_subgroup

deleted theorem submodule.pointwise_smul_to_add_submonoid

deleted theorem submodule.smul_le_self_of_tower

deleted theorem submodule.smul_mem_pointwise_smul

deleted theorem submodule.zero_eq_bot

Modified src/ring_theory/subring.lean

Modified src/topology/algebra/nonarchimedean/basic.lean