Commit 2024-05-21 09:04 333e8948

View on Github →

chore: Split Algebra.Group.Prod (#12974) Move the non-additivisable declarations to a new file Algebra.GroupWithZero.Prod. Credit Eric for https://github.com/leanprover-community/mathlib/pull/6866 and myself for https://github.com/leanprover-community/mathlib/pull/10907.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Group/Multiset.lean

Modified Mathlib/Algebra/BigOperators/Pi.lean

Modified Mathlib/Algebra/Function/Support.lean

Modified Mathlib/Algebra/Group/Conj.lean

Modified Mathlib/Algebra/Group/Prod.lean

deleted def divMonoidWithZeroHom

deleted def mulMonoidWithZeroHom

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

Created Mathlib/Algebra/GroupWithZero/Prod.lean

added def divMonoidWithZeroHom

added def mulMonoidWithZeroHom

Modified Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean

Modified Mathlib/Algebra/Order/Interval/Basic.lean

Modified Mathlib/Algebra/Order/Monoid/Prod.lean

Modified Mathlib/Algebra/Order/Sub/Prod.lean

Modified Mathlib/Algebra/Ring/Fin.lean

Modified Mathlib/Algebra/Ring/Prod.lean

Modified Mathlib/Algebra/SMulWithZero.lean

Modified Mathlib/Data/Finset/Card.lean

Modified Mathlib/Data/Multiset/Bind.lean

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

Modified Mathlib/Data/Nat/Pairing.lean

Modified Mathlib/GroupTheory/Congruence.lean

Modified Mathlib/GroupTheory/GroupAction/Prod.lean

Modified Mathlib/GroupTheory/NoncommCoprod.lean