Commit 2021-10-04 09:48 8a05dca7

View on Github →

feat(order/jordan_holder): Jordan Hölder theorem (#8976) The Jordan Hoelder theorem proved for a Jordan Hölder lattice, instances of which include submodules of a module and subgroups of a group.

Estimated changes

Created src/order/jordan_holder.lean

added def composition_series.append

added theorem composition_series.append_cast_add

added theorem composition_series.append_cast_add_aux

added theorem composition_series.append_nat_add

added theorem composition_series.append_nat_add_aux

added theorem composition_series.append_succ_cast_add

added theorem composition_series.append_succ_cast_add_aux

added theorem composition_series.append_succ_nat_add

added theorem composition_series.append_succ_nat_add_aux

added def composition_series.bot

added theorem composition_series.bot_erase_top

added theorem composition_series.bot_le

added theorem composition_series.bot_le_of_mem

added theorem composition_series.bot_mem

added theorem composition_series.bot_snoc

added theorem composition_series.chain'_to_list

added theorem composition_series.coe_fn_mk

added theorem composition_series.eq_of_bot_eq_bot_of_top_eq_top_of_length_eq_zero

added theorem composition_series.eq_snoc_erase_top

added theorem composition_series.equivalent.append

added theorem composition_series.equivalent.length_eq

added theorem composition_series.equivalent.refl

added theorem composition_series.equivalent.snoc_snoc_swap

added theorem composition_series.equivalent.symm

added theorem composition_series.equivalent.trans

added def composition_series.equivalent

added def composition_series.erase_top

added theorem composition_series.erase_top_top_le

added theorem composition_series.exists_top_eq_snoc_equivalant

added theorem composition_series.ext

added theorem composition_series.ext_fun

added theorem composition_series.forall_mem_eq_of_length_eq_zero

added theorem composition_series.is_maximal_erase_top_top

added theorem composition_series.jordan_holder

added theorem composition_series.le_top

added theorem composition_series.le_top_of_mem

added theorem composition_series.length_eq_zero_of_bot_eq_bot_of_top_eq_top_of_length_eq_zero

added theorem composition_series.length_of_list

added theorem composition_series.length_pos_of_bot_eq_bot_of_top_eq_top_of_length_pos

added theorem composition_series.length_pos_of_mem_ne

added theorem composition_series.length_to_list

added theorem composition_series.lt_succ

added theorem composition_series.lt_top_of_mem_erase_top

added theorem composition_series.mem_def

added theorem composition_series.mem_erase_top

added theorem composition_series.mem_erase_top_of_ne_of_mem

added theorem composition_series.mem_snoc

added theorem composition_series.mem_to_list

added def composition_series.of_list

added theorem composition_series.of_list_to_list'

added theorem composition_series.of_list_to_list

added def composition_series.snoc

added theorem composition_series.snoc_cast_succ

added theorem composition_series.snoc_erase_top_top

added theorem composition_series.snoc_last

added theorem composition_series.step

added def composition_series.to_list

added theorem composition_series.to_list_injective

added theorem composition_series.to_list_ne_nil

added theorem composition_series.to_list_nodup

added theorem composition_series.to_list_of_list

added theorem composition_series.to_list_sorted

added def composition_series.top

added theorem composition_series.top_erase_top

added theorem composition_series.top_mem

added theorem composition_series.top_snoc

added theorem composition_series.total

added structure composition_series

added theorem jordan_holder_lattice.is_maximal.iso_refl

added theorem jordan_holder_lattice.is_maximal_inf_right_of_is_maximal_sup

added theorem jordan_holder_lattice.is_maximal_of_eq_inf

added theorem jordan_holder_lattice.second_iso_of_eq