Commit 2024-07-17 17:39 7d65c07a

View on Github →

chore: Move order theory and algebra out of Data.Fin.Tuple.Basic (#13148)

  • Move the order theory in Data.Fin.Tuple.Basic to Order.Fin.Basic and a new file Order.Fin.Tuple
  • Move the content of Data.Fin.Tuple.Monotone to Order.Fin.Tuple
  • Move the algebra in Data.Fin.Tuple.Basic and Data.Fin.VecNotation to a new file Algebra.Group.Fin.Tuple

Estimated changes

added theorem Fin.insertNth_div
added theorem Fin.insertNth_div_same
added theorem Fin.insertNth_mul
added theorem Matrix.add_cons
added theorem Matrix.cons_add
added theorem Matrix.cons_add_cons
added theorem Matrix.cons_sub
added theorem Matrix.cons_sub_cons
added theorem Matrix.cons_zero_zero
added theorem Matrix.empty_add_empty
added theorem Matrix.empty_sub_empty
added theorem Matrix.head_add
added theorem Matrix.head_neg
added theorem Matrix.head_sub
added theorem Matrix.head_zero
added theorem Matrix.neg_cons
added theorem Matrix.neg_empty
added theorem Matrix.smul_cons
added theorem Matrix.smul_empty
added theorem Matrix.sub_cons
added theorem Matrix.tail_add
added theorem Matrix.tail_neg
added theorem Matrix.tail_sub
added theorem Matrix.tail_zero
added theorem Matrix.zero_empty
deleted theorem Fin.insertNth_add
deleted theorem Fin.insertNth_div
deleted theorem Fin.insertNth_mem_Icc
deleted theorem Fin.insertNth_mul
deleted theorem Fin.insertNth_sub
deleted theorem Fin.insertNth_sub_same
deleted theorem Fin.insertNth_zero_right
deleted theorem Fin.pi_lex_lt_cons_cons
deleted theorem Antitone.vecCons
deleted theorem Monotone.vecCons
deleted theorem StrictAnti.vecCons
deleted theorem StrictMono.vecCons
deleted theorem antitone_vecCons
deleted theorem antitone_vecEmpty
deleted theorem liftFun_vecCons
deleted theorem monotone_vecCons
deleted theorem monotone_vecEmpty
deleted theorem strictAnti_vecCons
deleted theorem strictAnti_vecEmpty
deleted theorem strictMono_vecCons
deleted theorem strictMono_vecEmpty
deleted theorem Matrix.add_cons
deleted theorem Matrix.cons_add
deleted theorem Matrix.cons_add_cons
deleted theorem Matrix.cons_eq_zero_iff
deleted theorem Matrix.cons_nonzero_iff
deleted theorem Matrix.cons_sub
deleted theorem Matrix.cons_sub_cons
deleted theorem Matrix.cons_zero_zero
deleted theorem Matrix.empty_add_empty
deleted theorem Matrix.empty_sub_empty
deleted theorem Matrix.head_add
deleted theorem Matrix.head_neg
deleted theorem Matrix.head_sub
deleted theorem Matrix.head_zero
deleted theorem Matrix.neg_cons
deleted theorem Matrix.neg_empty
deleted theorem Matrix.smul_cons
deleted theorem Matrix.smul_empty
deleted theorem Matrix.sub_cons
deleted theorem Matrix.tail_add
deleted theorem Matrix.tail_neg
deleted theorem Matrix.tail_sub
deleted theorem Matrix.tail_zero
deleted theorem Matrix.zero_empty
deleted def Fin.castLEOrderIso
added def Fin.castLEquiv
modified def finSuccAboveEquiv
added theorem Antitone.vecCons
added theorem Fin.insertNth_mem_Icc
added theorem Monotone.vecCons
added theorem StrictAnti.vecCons
added theorem StrictMono.vecCons
added theorem antitone_vecCons
added theorem antitone_vecEmpty
added theorem liftFun_vecCons
added theorem monotone_vecCons
added theorem monotone_vecEmpty
added theorem strictAnti_vecCons
added theorem strictAnti_vecEmpty
added theorem strictMono_vecCons
added theorem strictMono_vecEmpty