Commit 2021-07-28 00:40 37fc4cf4

View on Github →

feat(group_theory/subgroup): equiv_map_of_injective (#8371) Also for rings and submonoids. The version for modules, submodule.equiv_map_of_injective, was already there.

Estimated changes

Modified src/group_theory/subgroup.lean

added theorem subgroup.coe_equiv_map_of_injective_apply

Modified src/group_theory/submonoid/operations.lean

added theorem submonoid.coe_equiv_map_of_injective_apply

Modified src/linear_algebra/basic.lean

added theorem submodule.coe_equiv_map_of_injective_apply

Modified src/ring_theory/subring.lean

added theorem subring.coe_equiv_map_of_injective_apply

Modified src/ring_theory/subsemiring.lean

added theorem subsemiring.coe_equiv_map_of_injective_apply