Commit 2023-03-23 17:36 dcd3c890

View on Github →

feat: port GroupTheory.FreeProduct (#2979)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Unitization.lean

Modified Mathlib/Algebra/Free.lean

Modified Mathlib/Data/MvPolynomial/Basic.lean

Modified Mathlib/Data/Polynomial/AlgebraMap.lean

Created Mathlib/GroupTheory/FreeProduct.lean

added theorem FreeGroup.injective_lift_of_ping_pong

added theorem FreeProduct.NeWord.append_head

added theorem FreeProduct.NeWord.append_last

added theorem FreeProduct.NeWord.append_prod

added def FreeProduct.NeWord.head

added def FreeProduct.NeWord.inv

added theorem FreeProduct.NeWord.inv_head

added theorem FreeProduct.NeWord.inv_last

added theorem FreeProduct.NeWord.inv_prod

added def FreeProduct.NeWord.last

added def FreeProduct.NeWord.mulHead

added theorem FreeProduct.NeWord.mulHead_head

added theorem FreeProduct.NeWord.mulHead_prod

added theorem FreeProduct.NeWord.of_word

added def FreeProduct.NeWord.prod

added theorem FreeProduct.NeWord.prod_singleton

added def FreeProduct.NeWord.replaceHead

added theorem FreeProduct.NeWord.replaceHead_head

added theorem FreeProduct.NeWord.singleton_head

added theorem FreeProduct.NeWord.singleton_last

added def FreeProduct.NeWord.toList

added theorem FreeProduct.NeWord.toList_getLast?

added theorem FreeProduct.NeWord.toList_head?

added theorem FreeProduct.NeWord.toList_ne_nil

added def FreeProduct.NeWord.toWord

added inductive FreeProduct.NeWord

added inductive FreeProduct.Rel

added structure FreeProduct.Word.Pair

added theorem FreeProduct.Word.cons_eq_rcons

added theorem FreeProduct.Word.cons_eq_smul

added def FreeProduct.Word.empty

added def FreeProduct.Word.equiv

added def FreeProduct.Word.equivPair

added theorem FreeProduct.Word.equivPair_eq_of_fstIdx_ne

added theorem FreeProduct.Word.equivPair_symm

added def FreeProduct.Word.fstIdx

added theorem FreeProduct.Word.fstIdx_ne_iff

added theorem FreeProduct.Word.of_smul_def

added def FreeProduct.Word.prod

added theorem FreeProduct.Word.prod_empty

added theorem FreeProduct.Word.prod_rcons

added theorem FreeProduct.Word.prod_smul

added def FreeProduct.Word.rcons

added theorem FreeProduct.Word.rcons_inj

added theorem FreeProduct.Word.smul_induction

added structure FreeProduct.Word

added theorem FreeProduct.empty_of_word_prod_eq_one

added theorem FreeProduct.ext_hom

added theorem FreeProduct.induction_on

added theorem FreeProduct.inv_def

added def FreeProduct.lift

added theorem FreeProduct.lift_injective_of_ping_pong

added theorem FreeProduct.lift_mrange_le

added theorem FreeProduct.lift_of

added theorem FreeProduct.lift_range_le

added theorem FreeProduct.lift_word_ping_pong

added theorem FreeProduct.lift_word_prod_nontrivial_of_head_card

added theorem FreeProduct.lift_word_prod_nontrivial_of_head_eq_last

added theorem FreeProduct.lift_word_prod_nontrivial_of_not_empty

added theorem FreeProduct.lift_word_prod_nontrivial_of_other_i

added theorem FreeProduct.mrange_eq_supᵢ

added def FreeProduct.of

added theorem FreeProduct.of_apply

added theorem FreeProduct.of_injective

added theorem FreeProduct.of_leftInverse

added theorem FreeProduct.range_eq_supᵢ

added def FreeProduct

added def freeGroupEquivFreeProduct

Modified Mathlib/GroupTheory/IsFreeGroup.lean

Modified Mathlib/GroupTheory/QuotientGroup.lean

Modified Mathlib/LinearAlgebra/Quotient.lean