Commit 2023-03-08 14:42 b4c2472b

View on Github →

feat: port Order.JordanHolder (#2578)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/JordanHolder.lean

added theorem CompositionSeries.Equivalent.append

added theorem CompositionSeries.Equivalent.length_eq

added theorem CompositionSeries.Equivalent.refl

added theorem CompositionSeries.Equivalent.snoc_snoc_swap

added theorem CompositionSeries.Equivalent.symm

added theorem CompositionSeries.Equivalent.trans

added def CompositionSeries.Equivalent

added def CompositionSeries.append

added theorem CompositionSeries.append_castAdd

added theorem CompositionSeries.append_castAdd_aux

added theorem CompositionSeries.append_natAdd

added theorem CompositionSeries.append_natAdd_aux

added theorem CompositionSeries.append_succ_castAdd

added theorem CompositionSeries.append_succ_castAdd_aux

added theorem CompositionSeries.append_succ_natAdd

added theorem CompositionSeries.append_succ_natAdd_aux

added def CompositionSeries.bot

added theorem CompositionSeries.bot_eraseTop

added theorem CompositionSeries.bot_le

added theorem CompositionSeries.bot_le_of_mem

added theorem CompositionSeries.bot_mem

added theorem CompositionSeries.bot_snoc

added theorem CompositionSeries.chain'_toList

added theorem CompositionSeries.coeFn_mk

added theorem CompositionSeries.coe_append

added theorem CompositionSeries.eq_of_bot_eq_bot_of_top_eq_top_of_length_eq_zero

added theorem CompositionSeries.eq_snoc_eraseTop

added def CompositionSeries.eraseTop

added theorem CompositionSeries.eraseTop_top_le

added theorem CompositionSeries.exists_top_eq_snoc_equivalant

added theorem CompositionSeries.ext

added theorem CompositionSeries.ext_fun

added theorem CompositionSeries.forall_mem_eq_of_length_eq_zero

added theorem CompositionSeries.isMaximal_eraseTop_top

added theorem CompositionSeries.jordan_holder

added theorem CompositionSeries.le_top

added theorem CompositionSeries.le_top_of_mem

added theorem CompositionSeries.length_eq_zero_of_bot_eq_bot_of_top_eq_top_of_length_eq_zero

added theorem CompositionSeries.length_ofList

added theorem CompositionSeries.length_pos_of_bot_eq_bot_of_top_eq_top_of_length_pos

added theorem CompositionSeries.length_pos_of_mem_ne

added theorem CompositionSeries.length_toList

added theorem CompositionSeries.lt_succ

added theorem CompositionSeries.lt_top_of_mem_eraseTop

added theorem CompositionSeries.mem_def

added theorem CompositionSeries.mem_eraseTop

added theorem CompositionSeries.mem_eraseTop_of_ne_of_mem

added theorem CompositionSeries.mem_snoc

added theorem CompositionSeries.mem_toList

added def CompositionSeries.ofList

added theorem CompositionSeries.ofList_toList'

added theorem CompositionSeries.ofList_toList

added def CompositionSeries.snoc

added theorem CompositionSeries.snoc_castSucc

added theorem CompositionSeries.snoc_eraseTop_top

added theorem CompositionSeries.snoc_last

added theorem CompositionSeries.step

added def CompositionSeries.toList

added theorem CompositionSeries.toList_injective

added theorem CompositionSeries.toList_ne_nil

added theorem CompositionSeries.toList_nodup

added theorem CompositionSeries.toList_ofList

added theorem CompositionSeries.toList_sorted

added def CompositionSeries.top

added theorem CompositionSeries.top_eraseTop

added theorem CompositionSeries.top_mem

added theorem CompositionSeries.top_snoc

added theorem CompositionSeries.total

added structure CompositionSeries

added theorem JordanHolderLattice.IsMaximal.iso_refl

added theorem JordanHolderLattice.isMaximal_inf_right_of_isMaximal_sup

added theorem JordanHolderLattice.isMaximal_of_eq_inf

added theorem JordanHolderLattice.second_iso_of_eq