Commit 2023-12-10 22:40 7df4ff91

View on Github →

chore: reduce imports of Data.List.Defs (#8635) Currently Data.List.Defs depends on Algebra.Group.Defs, rather unnecessarily. (This then prevents importing Data.List.Defs into Tactic.Common, without breaking various assert_not_exists statements.)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/List/BigOperators/Basic.lean

added theorem List.rel_prod

Created Mathlib/Data/List/BigOperators/Defs.lean

added def List.alternatingProd

added def List.alternatingSum

added def List.prod

Modified Mathlib/Data/List/Defs.lean

deleted def List.alternatingProd

deleted def List.alternatingSum

deleted def List.prod

deleted def List.sum

Modified Mathlib/Data/List/Forall2.lean

deleted theorem List.rel_prod

Modified test/congr.lean

Modified test/convert2.lean