Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-11 10:25 ea0fb11b

View on Github →

style(group_theory): try to follow conventions (calc indentation, lowercase names, ...)

Estimated changes

Modified group_theory/coset.lean

modified theorem eq_cosets_of_normal

modified def left_coset

modified theorem left_coset_assoc

modified def left_coset_equiv

modified theorem left_coset_equiv_rel

modified theorem left_coset_mem_left_coset

modified theorem left_coset_right_coset

modified theorem mem_left_coset

modified theorem mem_left_coset_left_coset

modified theorem mem_mem_left_coset

modified theorem mem_own_left_coset

modified theorem mem_own_right_coset

modified theorem mem_right_coset

modified theorem mem_right_coset_right_coset

modified theorem normal_iff_eq_cosets

modified theorem normal_of_eq_cosets

modified theorem one_left_coset

modified theorem one_right_coset

modified def right_coset

modified theorem right_coset_assoc

modified theorem right_coset_mem_right_coset

Modified group_theory/subgroup.lean

modified def cosets

modified theorem injective_mul

modified theorem is_group_hom.inj_iff_trivial_kernel

modified theorem is_group_hom.inj_of_trivial_kernel

modified theorem is_group_hom.inv_iff_ker

modified theorem is_group_hom.inv_ker

modified theorem is_group_hom.inv_ker_one

modified theorem is_group_hom.ker_inv

modified def is_group_hom.kernel

modified theorem is_group_hom.mem_ker_one

modified theorem is_group_hom.one_iff_ker_inv

modified theorem is_group_hom.one_ker_inv

modified theorem is_group_hom.trivial_kernel_of_inj

modified def is_subgroup.center

modified theorem is_subgroup.eq_one_of_trivial_mem

modified theorem is_subgroup.mem_norm_comm

modified def is_subgroup.trivial

modified theorem is_subgroup.trivial_mem_of_eq_one