mathlib
60ad8448 - feat(group_theory/complement): API lemmas relating `range_mem_transversals` and `to_equiv` (#13694)

Commit
3 years ago
feat(group_theory/complement): API lemmas relating `range_mem_transversals` and `to_equiv` (#13694) This PR adds an API lemma relating `range_mem_left_transversals` (the main way of constructing left transversals) and `mem_left_transversals.to_equiv` (one of the main constructions from left transversals), and a similar lemma relating the right versions.
Author
Parents
Loading