Commit 2021-07-28 21:04 92a5be8d

View on Github →

feat(ring,group,monoid): map_equiv lemmas for different structures (#8453) There is some inconsistency in the statements of these lemmas because there is a coercion from ring_equiv to ring_hom, but not mul_equiv to monoid_hom.

Estimated changes

Modified src/data/equiv/basic.lean

added theorem set.image_equiv_eq_preimage_symm

added theorem set.mem_image_equiv

added theorem set.preimage_equiv_eq_image_symm

Modified src/group_theory/subgroup.lean

added theorem subgroup.comap_equiv_eq_map_symm

added theorem subgroup.map_equiv_eq_comap_symm

added theorem subgroup.mem_map_equiv

Modified src/group_theory/submonoid/operations.lean

added theorem submonoid.comap_equiv_eq_map_symm

added theorem submonoid.map_equiv_eq_comap_symm

added theorem submonoid.mem_map_equiv

Modified src/linear_algebra/basic.lean

added theorem submodule.comap_equiv_eq_map_symm

added theorem submodule.map_equiv_eq_comap_symm

Modified src/ring_theory/subring.lean

added theorem subring.comap_equiv_eq_map_symm

added theorem subring.map_equiv_eq_comap_symm

added theorem subring.mem_map_equiv

Modified src/ring_theory/subsemiring.lean

added theorem subsemiring.comap_equiv_eq_map_symm

added theorem subsemiring.map_equiv_eq_comap_symm

added theorem subsemiring.mem_map_equiv