Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-11 13:50 d2ab199f

View on Github →

chore(group_theory): simplify proofs; generalize some theorems

Estimated changes

modified theorem eq_cosets_of_normal
modified theorem left_coset_assoc
modified theorem left_coset_right_coset
added theorem mem_left_coset_iff
deleted theorem mem_mem_left_coset
added theorem mem_right_coset_iff
modified theorem normal_of_eq_cosets
modified theorem one_left_coset
deleted theorem one_right_coset
modified theorem right_coset_assoc
added theorem right_coset_one
modified theorem is_group_hom.inv_iff_ker
deleted theorem is_group_hom.inv_ker
added def is_group_hom.ker
deleted theorem is_group_hom.ker_inv
deleted def is_group_hom.kernel
added theorem is_group_hom.mem_ker
deleted theorem is_group_hom.mem_ker_one
modified theorem is_group_hom.one_ker_inv
added theorem is_subgroup.mem_center
modified theorem is_subgroup.mem_norm_comm