Commit 2023-07-31 14:06 15677ddc

View on Github →

refactor: rename FreeProduct to Monoid.CoprodI (#6055)

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/GroupTheory/FreeProduct.lean to Mathlib/GroupTheory/CoprodI.lean

deleted theorem FreeProduct.NeWord.append_head

deleted theorem FreeProduct.NeWord.append_last

deleted theorem FreeProduct.NeWord.append_prod

deleted def FreeProduct.NeWord.head

deleted def FreeProduct.NeWord.inv

deleted theorem FreeProduct.NeWord.inv_head

deleted theorem FreeProduct.NeWord.inv_last

deleted theorem FreeProduct.NeWord.inv_prod

deleted def FreeProduct.NeWord.last

deleted def FreeProduct.NeWord.mulHead

deleted theorem FreeProduct.NeWord.mulHead_head

deleted theorem FreeProduct.NeWord.mulHead_prod

deleted theorem FreeProduct.NeWord.of_word

deleted def FreeProduct.NeWord.prod

deleted theorem FreeProduct.NeWord.prod_singleton

deleted def FreeProduct.NeWord.replaceHead

deleted theorem FreeProduct.NeWord.replaceHead_head

deleted theorem FreeProduct.NeWord.singleton_head

deleted theorem FreeProduct.NeWord.singleton_last

deleted def FreeProduct.NeWord.toList

deleted theorem FreeProduct.NeWord.toList_getLast?

deleted theorem FreeProduct.NeWord.toList_head?

deleted theorem FreeProduct.NeWord.toList_ne_nil

deleted def FreeProduct.NeWord.toWord

deleted inductive FreeProduct.NeWord

deleted inductive FreeProduct.Rel

deleted structure FreeProduct.Word.Pair

deleted theorem FreeProduct.Word.cons_eq_rcons

deleted theorem FreeProduct.Word.cons_eq_smul

deleted def FreeProduct.Word.empty

deleted def FreeProduct.Word.equiv

deleted def FreeProduct.Word.equivPair

deleted theorem FreeProduct.Word.equivPair_eq_of_fstIdx_ne

deleted theorem FreeProduct.Word.equivPair_symm

deleted def FreeProduct.Word.fstIdx

deleted theorem FreeProduct.Word.fstIdx_ne_iff

deleted theorem FreeProduct.Word.of_smul_def

deleted def FreeProduct.Word.prod

deleted theorem FreeProduct.Word.prod_empty

deleted theorem FreeProduct.Word.prod_rcons

deleted theorem FreeProduct.Word.prod_smul

deleted def FreeProduct.Word.rcons

deleted theorem FreeProduct.Word.rcons_inj

deleted theorem FreeProduct.Word.smul_induction

deleted structure FreeProduct.Word

deleted theorem FreeProduct.empty_of_word_prod_eq_one

deleted theorem FreeProduct.ext_hom

deleted theorem FreeProduct.induction_on

deleted theorem FreeProduct.inv_def

deleted def FreeProduct.lift

deleted theorem FreeProduct.lift_injective_of_ping_pong

deleted theorem FreeProduct.lift_mrange_le

deleted theorem FreeProduct.lift_of

deleted theorem FreeProduct.lift_range_le

deleted theorem FreeProduct.lift_word_ping_pong

deleted theorem FreeProduct.lift_word_prod_nontrivial_of_head_card

deleted theorem FreeProduct.lift_word_prod_nontrivial_of_head_eq_last

deleted theorem FreeProduct.lift_word_prod_nontrivial_of_not_empty

deleted theorem FreeProduct.lift_word_prod_nontrivial_of_other_i

deleted theorem FreeProduct.mrange_eq_iSup

deleted def FreeProduct.of

deleted theorem FreeProduct.of_apply

deleted theorem FreeProduct.of_injective

deleted theorem FreeProduct.of_leftInverse

deleted theorem FreeProduct.range_eq_iSup

deleted def FreeProduct

added theorem Monoid.CoprodI.NeWord.append_head

added theorem Monoid.CoprodI.NeWord.append_last

added theorem Monoid.CoprodI.NeWord.append_prod

added def Monoid.CoprodI.NeWord.head

added def Monoid.CoprodI.NeWord.inv

added theorem Monoid.CoprodI.NeWord.inv_head

added theorem Monoid.CoprodI.NeWord.inv_last

added theorem Monoid.CoprodI.NeWord.inv_prod

added def Monoid.CoprodI.NeWord.last

added def Monoid.CoprodI.NeWord.mulHead

added theorem Monoid.CoprodI.NeWord.mulHead_head

added theorem Monoid.CoprodI.NeWord.mulHead_prod

added theorem Monoid.CoprodI.NeWord.of_word

added def Monoid.CoprodI.NeWord.prod

added theorem Monoid.CoprodI.NeWord.prod_singleton

added def Monoid.CoprodI.NeWord.replaceHead

added theorem Monoid.CoprodI.NeWord.replaceHead_head

added theorem Monoid.CoprodI.NeWord.singleton_head

added theorem Monoid.CoprodI.NeWord.singleton_last

added def Monoid.CoprodI.NeWord.toList

added theorem Monoid.CoprodI.NeWord.toList_getLast?

added theorem Monoid.CoprodI.NeWord.toList_head?

added theorem Monoid.CoprodI.NeWord.toList_ne_nil

added def Monoid.CoprodI.NeWord.toWord

added inductive Monoid.CoprodI.NeWord

added inductive Monoid.CoprodI.Rel

added structure Monoid.CoprodI.Word.Pair

added theorem Monoid.CoprodI.Word.cons_eq_rcons

added theorem Monoid.CoprodI.Word.cons_eq_smul

added def Monoid.CoprodI.Word.empty

added def Monoid.CoprodI.Word.equiv

added def Monoid.CoprodI.Word.equivPair

added theorem Monoid.CoprodI.Word.equivPair_eq_of_fstIdx_ne

added theorem Monoid.CoprodI.Word.equivPair_symm

added def Monoid.CoprodI.Word.fstIdx

added theorem Monoid.CoprodI.Word.fstIdx_ne_iff

added theorem Monoid.CoprodI.Word.of_smul_def

added def Monoid.CoprodI.Word.prod

added theorem Monoid.CoprodI.Word.prod_empty

added theorem Monoid.CoprodI.Word.prod_rcons

added theorem Monoid.CoprodI.Word.prod_smul

added def Monoid.CoprodI.Word.rcons

added theorem Monoid.CoprodI.Word.rcons_inj

added theorem Monoid.CoprodI.Word.smul_induction

added structure Monoid.CoprodI.Word

added theorem Monoid.CoprodI.empty_of_word_prod_eq_one

added theorem Monoid.CoprodI.ext_hom

added theorem Monoid.CoprodI.induction_on

added theorem Monoid.CoprodI.inv_def

added def Monoid.CoprodI.lift

added theorem Monoid.CoprodI.lift_injective_of_ping_pong

added theorem Monoid.CoprodI.lift_mrange_le

added theorem Monoid.CoprodI.lift_of

added theorem Monoid.CoprodI.lift_range_le

added theorem Monoid.CoprodI.lift_word_ping_pong

added theorem Monoid.CoprodI.lift_word_prod_nontrivial_of_head_card

added theorem Monoid.CoprodI.lift_word_prod_nontrivial_of_head_eq_last

added theorem Monoid.CoprodI.lift_word_prod_nontrivial_of_not_empty

added theorem Monoid.CoprodI.lift_word_prod_nontrivial_of_other_i

added theorem Monoid.CoprodI.mrange_eq_iSup

added def Monoid.CoprodI.of

added theorem Monoid.CoprodI.of_apply

added theorem Monoid.CoprodI.of_injective

added theorem Monoid.CoprodI.of_leftInverse

added theorem Monoid.CoprodI.range_eq_iSup

added def Monoid.CoprodI

added def freeGroupEquivCoprodI

deleted def freeGroupEquivFreeProduct