Commit 2024-11-22 08:58 8e3e89e9

View on Github →

chore: split Algebra.Group.TypeTags (#19351)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/Grp/FiniteGrp.lean

Modified Mathlib/Algebra/FreeMonoid/Count.lean

Modified Mathlib/Algebra/Group/Action/TypeTags.lean

Modified Mathlib/Algebra/Group/Equiv/TypeTags.lean

Modified Mathlib/Algebra/Group/Even.lean

Modified Mathlib/Algebra/Group/Subgroup/Map.lean

Modified Mathlib/Algebra/Group/Subsemigroup/Operations.lean

Renamed Mathlib/Algebra/Group/TypeTags.lean to Mathlib/Algebra/Group/TypeTags/Basic.lean

deleted theorem AddMonoidHom.coe_toMultiplicative''

deleted theorem AddMonoidHom.coe_toMultiplicative'

deleted theorem AddMonoidHom.coe_toMultiplicative

deleted def AddMonoidHom.toMultiplicative''

deleted def AddMonoidHom.toMultiplicative'

deleted def AddMonoidHom.toMultiplicative

deleted theorem MonoidHom.coe_toAdditive''

deleted theorem MonoidHom.coe_toAdditive'

deleted theorem MonoidHom.coe_toMultiplicative

deleted def MonoidHom.toAdditive''

deleted def MonoidHom.toAdditive'

deleted def MonoidHom.toAdditive

Created Mathlib/Algebra/Group/TypeTags/Finite.lean

Created Mathlib/Algebra/Group/TypeTags/Hom.lean

added theorem AddMonoidHom.coe_toMultiplicative''

added theorem AddMonoidHom.coe_toMultiplicative'

added theorem AddMonoidHom.coe_toMultiplicative

added def AddMonoidHom.toMultiplicative''

added def AddMonoidHom.toMultiplicative'

added def AddMonoidHom.toMultiplicative

added theorem MonoidHom.coe_toAdditive''

added theorem MonoidHom.coe_toAdditive'

added theorem MonoidHom.coe_toMultiplicative

added def MonoidHom.toAdditive''

added def MonoidHom.toAdditive'

added def MonoidHom.toAdditive

Modified Mathlib/Algebra/Order/Monoid/Unbundled/TypeTags.lean

Modified Mathlib/Analysis/Normed/Field/Lemmas.lean

Modified Mathlib/Data/Finsupp/Defs.lean

Modified Mathlib/Data/Fintype/Basic.lean

Modified Mathlib/Data/Nat/Cast/Basic.lean

Modified Mathlib/Deprecated/Group.lean

Modified Mathlib/GroupTheory/FiniteAbelian/Basic.lean