Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-26 20:12 d4343972

View on Github →

feat(group_theory/conjugates) : define conjugates (#1029)

feat(algebra/order_functions): generalize strict_mono.monotone (#1022)
moving stuff to where it belongs
removed unecessary import
Changed to union
Update src/group_theory/subgroup.lean Co-Authored-By: Johan Commelin johan@commelin.net
Stylistic changes
Added authorship
Moved mem_conjugates_of_set
Authorship
Trying fixes
Putting everything in the right order
removed import

Estimated changes

Modified src/algebra/group.lean

added theorem conj_inv

added theorem conj_mul

Modified src/group_theory/subgroup.lean

added theorem group.conj_mem_conjugates_of_set

added def group.conjugates

added def group.conjugates_of_set

added theorem group.conjugates_of_set_mono

added theorem group.conjugates_of_set_subset

added theorem group.conjugates_of_set_subset_normal_closure

added theorem group.conjugates_subset

added theorem group.mem_conjugates_of_set_iff

added theorem group.mem_conjugates_self

added def group.normal_closure

added theorem group.normal_closure_mono

added theorem group.normal_closure_subset

added theorem group.normal_closure_subset_iff

added theorem group.subset_conjugates_of_set

added theorem group.subset_normal_closure