Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-11 10:24 fa86d349

View on Github →

feat(group_theory): add left/right cosets and normal subgroups

Estimated changes

modified theorem is_group_anti_hom.prod
modified theorem is_group_hom.prod
modified theorem is_group_anti_hom.inv
modified theorem is_group_anti_hom.mul
modified theorem is_group_hom.inv
modified theorem is_group_hom.mul
modified def is_group_hom
added theorem eq_cosets_of_normal
added def left_coset
added theorem left_coset_assoc
added def left_coset_equiv
added theorem left_coset_equiv_rel
added theorem left_coset_right_coset
added theorem mem_left_coset
added theorem mem_mem_left_coset
added theorem mem_own_left_coset
added theorem mem_own_right_coset
added theorem mem_right_coset
added theorem normal_iff_eq_cosets
added theorem normal_of_eq_cosets
added theorem one_left_coset
added theorem one_right_coset
added def right_coset
added theorem right_coset_assoc
added theorem is_group_hom.inv_ker
added theorem is_group_hom.ker_inv