Mathlib v3 is deprecated. Go to Mathlib v4

Theorem doset.rel_bot_eq_right_group_rel

Modification history

2022-03-10 07:37
src/group_theory/double_coset.lean
feat(group_theory/double_cosets): definition of double cosets and some basic lemmas. (#9490) …
Added doset.rel_bot_eq_right_group_relView on Github →