Commit 2023-09-06 11:21 73877f41

View on Github →

feat(GroupTheory/CoprodI): add various things (#6900) The main changes made here were

Adding a cons constructor to make a new word where the underlying list is just cons. Use this to simplify the definition of rcons
Defining a consRecOn induction principle and use this to simpllify the definition of equivPairAux, allowing me to delete the private def mkAux
Some lemmas about being an element of rcons and smul

Estimated changes

Modified Mathlib/GroupTheory/CoprodI.lean

added def Monoid.CoprodI.Word.cons

added def Monoid.CoprodI.Word.consRecOn

added theorem Monoid.CoprodI.Word.consRecOn_cons

added theorem Monoid.CoprodI.Word.consRecOn_empty

deleted theorem Monoid.CoprodI.Word.cons_eq_rcons

added theorem Monoid.CoprodI.Word.equivPair_head

added theorem Monoid.CoprodI.Word.equivPair_head_smul_equivPair_tail

added theorem Monoid.CoprodI.Word.equivPair_smul_same

added theorem Monoid.CoprodI.Word.equivPair_tail

added theorem Monoid.CoprodI.Word.equivPair_tail_eq_inv_smul

added theorem Monoid.CoprodI.Word.fstIdx_cons

added theorem Monoid.CoprodI.Word.mem_equivPair_tail_iff

added theorem Monoid.CoprodI.Word.mem_of_mem_equivPair_tail

added theorem Monoid.CoprodI.Word.mem_rcons_iff

added theorem Monoid.CoprodI.Word.mem_smul_iff

added theorem Monoid.CoprodI.Word.mem_smul_iff_of_ne

added theorem Monoid.CoprodI.Word.prod_cons

added theorem Monoid.CoprodI.Word.rcons_eq_smul

added theorem Monoid.CoprodI.Word.smul_def

added theorem Monoid.CoprodI.Word.smul_eq_of_smul