Commit 2020-10-08 23:44 8004fb68

View on Github →

chore(topology/algebra/group): move a lemma to group_theory/coset (#4522) quotient_group_saturate didn't use any topology. Move it to group_theory/coset and rename to quotient_group.preimage_image_coe. Also rename quotient_group.open_coe to quotient_group.is_open_map_coe

Estimated changes

Modified src/group_theory/coset.lean

added theorem quotient_group.preimage_image_coe

Modified src/group_theory/quotient_group.lean

modified theorem quotient_group.coe_gpow

modified theorem quotient_group.coe_inv

modified theorem quotient_group.coe_mul

modified theorem quotient_group.coe_one

modified theorem quotient_group.coe_pow

Modified src/topology/algebra/group.lean

added theorem quotient_group.is_open_map_coe

deleted theorem quotient_group.open_coe

deleted theorem quotient_group_saturate