Mathlib v3 is deprecated. Go to Mathlib v4

Theorem group.conjugates_of_subset

Modification history

2021-08-01 17:17

src/deprecated/subgroup.lean

chore(deprecated/*): Make deprecated classes into structures (#8178) …

Modified group.conjugates_of_subset View on Github →

2021-04-06 18:32

src/deprecated/subgroup.lean

feat(algebra/group/conj): `is_conj` for `monoid`s, `is_conj.setoid`, and `conj_classes` (#6896) …

Added group.conjugates_of_subset View on Github →