Mathlib Changelog
v3
Changelog
About
Github
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