Commit 2023-09-06 07:39 b5528b3b

View on Github →

chore: cleanup Mathlib.Init.Data.Prod (#6972) Removing from Mathlib.Init.Data.Prod from the early parts of the import hierarchy. While at it, remove unnecessary uses of Prod.mk.eta across the library.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Basic.lean

Modified Mathlib/Algebra/BigOperators/Finprod.lean

Modified Mathlib/Algebra/EuclideanDomain/Basic.lean

Modified Mathlib/Algebra/EuclideanDomain/Defs.lean

Modified Mathlib/Algebra/Group/Prod.lean

Modified Mathlib/Algebra/Ring/Prod.lean

Modified Mathlib/Algebra/Support.lean

Modified Mathlib/Analysis/Convex/Extreme.lean

Modified Mathlib/Analysis/Convolution.lean

Modified Mathlib/Combinatorics/SimpleGraph/Prod.lean

Modified Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean

Modified Mathlib/Data/Finsupp/Basic.lean

Modified Mathlib/Data/Pi/Algebra.lean

Modified Mathlib/Data/Prod/Basic.lean

added theorem Prod.mk.eta

Modified Mathlib/Data/Prod/PProd.lean

Modified Mathlib/Data/Seq/Parallel.lean

Modified Mathlib/Data/Sym/Sym2.lean

Modified Mathlib/Geometry/Manifold/Algebra/Structures.lean

Modified Mathlib/Geometry/Manifold/ContMDiff.lean

Modified Mathlib/Geometry/Manifold/MFDeriv.lean

Modified Mathlib/GroupTheory/MonoidLocalization.lean

Modified Mathlib/Init/Data/Prod.lean

deleted theorem Prod.mk.eta

Modified Mathlib/Init/Function.lean

Modified Mathlib/LinearAlgebra/Finsupp.lean

Modified Mathlib/LinearAlgebra/Matrix/Determinant.lean

Modified Mathlib/LinearAlgebra/Prod.lean

Modified Mathlib/Logic/Equiv/Basic.lean

Modified Mathlib/Order/Filter/Prod.lean

Modified Mathlib/Order/Interval.lean

Modified Mathlib/Probability/Kernel/Composition.lean

Modified Mathlib/Probability/Kernel/MeasurableIntegral.lean

Modified Mathlib/Topology/EMetricSpace/Paracompact.lean

Modified Mathlib/Topology/FiberBundle/Trivialization.lean

Modified Mathlib/Topology/MetricSpace/MetrizableUniformity.lean

Modified lakefile.lean

modified def weakLeanArgs