Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-10 07:36 f985e364

View on Github →

feat(group_theory/subgroup): add mem_map_of_mem (#7459) From LTE. Written by @PatrickMassot

Estimated changes

Modified src/group_theory/subgroup.lean

added theorem subgroup.apply_coe_mem_map

added theorem subgroup.mem_map_of_mem

Modified src/group_theory/submonoid/operations.lean

added theorem submonoid.apply_coe_mem_map

modified theorem submonoid.mem_map_of_mem

Modified src/linear_algebra/basic.lean

added theorem submodule.apply_coe_mem_map

Modified src/ring_theory/jacobson.lean

Modified src/ring_theory/localization.lean