mathlib3
8004fb68 - chore(topology/algebra/group): move a lemma to `group_theory/coset` (#4522)

Commit
5 years ago
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`
Author
Parents
Loading