Commit 2023-11-14 15:34 a107e34d

View on Github →

feat: amalgamated products of groups (#6803)

Estimated changes

Modified Mathlib/GroupTheory/PushoutI.lean

added structure Monoid.PushoutI.NormalWord.Pair

added structure Monoid.PushoutI.NormalWord.Transversal

added theorem Monoid.PushoutI.NormalWord.base_smul_def'

added theorem Monoid.PushoutI.NormalWord.base_smul_def

added theorem Monoid.PushoutI.NormalWord.base_smul_eq_smul

added theorem Monoid.PushoutI.NormalWord.cons_eq_smul

added def Monoid.PushoutI.NormalWord.empty

added theorem Monoid.PushoutI.NormalWord.eq_one_of_smul_normalized

added theorem Monoid.PushoutI.NormalWord.ext

added theorem Monoid.PushoutI.NormalWord.ext_iff

added theorem Monoid.PushoutI.NormalWord.ext_smul

added theorem Monoid.PushoutI.NormalWord.of_smul_eq_smul

added def Monoid.PushoutI.NormalWord.prod

added theorem Monoid.PushoutI.NormalWord.prod_base_smul

added theorem Monoid.PushoutI.NormalWord.prod_cons

added theorem Monoid.PushoutI.NormalWord.prod_empty

added theorem Monoid.PushoutI.NormalWord.prod_injective

added theorem Monoid.PushoutI.NormalWord.prod_smul

added theorem Monoid.PushoutI.NormalWord.prod_smul_empty

added theorem Monoid.PushoutI.NormalWord.prod_summand_smul

added theorem Monoid.PushoutI.NormalWord.rcons_injective

added theorem Monoid.PushoutI.NormalWord.summand_smul_def'

added theorem Monoid.PushoutI.NormalWord.summand_smul_def

added theorem Monoid.PushoutI.NormalWord.transversal_nonempty

added structure Monoid.PushoutI.NormalWord

added theorem Monoid.PushoutI.Reduced.eq_empty_of_mem_range

added theorem Monoid.PushoutI.Reduced.exists_normalWord_prod_eq

added def Monoid.PushoutI.Reduced

added theorem Monoid.PushoutI.base_injective

added theorem Monoid.PushoutI.inf_of_range_eq_base_range

added theorem Monoid.PushoutI.of_injective