Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-20 11:48 e41e9bce

View on Github →

chore(group_theory/submonoid/operations): split a file (#9292)

Estimated changes

Modified src/group_theory/subgroup.lean

Modified src/group_theory/submonoid/operations.lean

deleted theorem add_submonoid.coe_pointwise_smul

deleted theorem add_submonoid.smul_mem_pointwise_smul

deleted theorem submonoid.coe_pointwise_smul

deleted theorem submonoid.smul_mem_pointwise_smul

Created src/group_theory/submonoid/pointwise.lean

added theorem add_submonoid.coe_pointwise_smul

added theorem add_submonoid.smul_mem_pointwise_smul

added theorem submonoid.coe_pointwise_smul

added theorem submonoid.smul_mem_pointwise_smul