Commit 2024-06-08 09:11 89f03043

View on Github →

chore: Rename Prod_map (#12753) ... in lemma names and section names in order to follow the naming convention.

Estimated changes

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

Modified Mathlib/Algebra/Group/Prod.lean

Modified Mathlib/Algebra/Ring/Prod.lean

Modified Mathlib/Analysis/Calculus/ContDiff/Basic.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Prod.lean

Modified Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean

Modified Mathlib/Combinatorics/Additive/Corner/Roth.lean

Modified Mathlib/Combinatorics/Additive/FreimanHom.lean

Modified Mathlib/Data/Countable/Basic.lean

Modified Mathlib/Data/Finset/Lattice.lean

Modified Mathlib/Data/Finsupp/Antidiagonal.lean

Modified Mathlib/Data/List/NatAntidiagonal.lean

Modified Mathlib/Data/List/Sublists.lean

Modified Mathlib/Data/Multiset/NatAntidiagonal.lean

Modified Mathlib/Data/Multiset/Powerset.lean

Modified Mathlib/Data/Prod/Basic.lean

deleted theorem Function.Bijective.Prod_map

added theorem Function.Bijective.prodMap

deleted theorem Function.Injective.Prod_map

added theorem Function.Injective.prodMap

deleted theorem Function.Involutive.Prod_map

added theorem Function.Involutive.prodMap

deleted theorem Function.LeftInverse.Prod_map

added theorem Function.LeftInverse.prodMap

deleted theorem Function.RightInverse.Prod_map

added theorem Function.RightInverse.prodMap

deleted theorem Function.Surjective.Prod_map

added theorem Function.Surjective.prodMap

added theorem Prod.map_apply

deleted theorem Prod_map

Modified Mathlib/FieldTheory/Perfect.lean

Modified Mathlib/Geometry/Manifold/ContMDiff/Product.lean

Modified Mathlib/LinearAlgebra/Dual.lean

Modified Mathlib/Logic/Embedding/Basic.lean

Modified Mathlib/Order/RelIso/Basic.lean

Modified Mathlib/RingTheory/Kaehler.lean

Modified Mathlib/Topology/Algebra/Group/Basic.lean

Modified Mathlib/Topology/Algebra/Module/Basic.lean

Modified Mathlib/Topology/DenseEmbedding.lean

Modified Mathlib/Topology/EMetricSpace/Basic.lean

Modified Mathlib/Topology/Inseparable.lean

Modified Mathlib/Topology/MetricSpace/Isometry.lean

Modified Mathlib/Topology/MetricSpace/PseudoMetric.lean

Modified Mathlib/Topology/UniformSpace/Cauchy.lean

Modified Mathlib/Topology/UniformSpace/Separation.lean

Modified Mathlib/Topology/UniformSpace/UniformConvergence.lean

Modified Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

Modified Mathlib/Topology/UniformSpace/UniformEmbedding.lean