Commit 2025-03-07 13:46 e051a2fa

View on Github →

chore: rename injectivity of Prod.mk lemmas (#22634) The current names are ancient and do not reflect the naming convention anymore.

Estimated changes

Modified Archive/Sensitivity.lean

Modified Archive/Wiedijk100Theorems/Partition.lean

Modified Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean

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

Modified Mathlib/Algebra/Group/End.lean

Modified Mathlib/Algebra/Group/Prod.lean

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

Modified Mathlib/Algebra/GroupWithZero/Action/Prod.lean

Modified Mathlib/Algebra/Module/Prod.lean

Modified Mathlib/Algebra/NoZeroSMulDivisors/Prod.lean

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

Modified Mathlib/Algebra/Order/Group/PosPart.lean

Modified Mathlib/Algebra/Ring/Prod.lean

Modified Mathlib/Algebra/ZeroOne/Prod.lean

modified theorem Prod.mk_eq_one

Modified Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean

Modified Mathlib/Analysis/Convex/Integral.lean

Modified Mathlib/Analysis/Convolution.lean

Modified Mathlib/Analysis/SpecialFunctions/PolarCoord.lean

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

Modified Mathlib/Combinatorics/Additive/Energy.lean

Modified Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean

Modified Mathlib/Combinatorics/SimpleGraph/Density.lean

Modified Mathlib/Combinatorics/SimpleGraph/Triangle/Counting.lean

Modified Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean

Modified Mathlib/Data/Countable/Basic.lean

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

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

Modified Mathlib/Data/Finset/Prod.lean

modified theorem Finset.product_singleton

Modified Mathlib/Data/List/ProdSigma.lean

Modified Mathlib/Data/List/Sublists.lean

Modified Mathlib/Data/Matrix/Basis.lean

Modified Mathlib/Data/Matrix/Block.lean

Modified Mathlib/Data/Multiset/Fintype.lean

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

Modified Mathlib/Data/Prod/Basic.lean

deleted theorem Prod.mk.inj_iff

deleted theorem Prod.mk.inj_left

deleted theorem Prod.mk.inj_right

added theorem Prod.mk_inj

deleted theorem Prod.mk_inj_left

deleted theorem Prod.mk_inj_right

added theorem Prod.mk_left_inj

added theorem Prod.mk_left_injective

added theorem Prod.mk_right_inj

added theorem Prod.mk_right_injective

Modified Mathlib/Data/Set/Pairwise/Lattice.lean

Modified Mathlib/Data/Sym/Card.lean

Modified Mathlib/Data/Sym/Sym2.lean

Modified Mathlib/FieldTheory/PolynomialGaloisGroup.lean

Modified Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

Modified Mathlib/Geometry/Manifold/WhitneyEmbedding.lean

Modified Mathlib/GroupTheory/Perm/Cycle/Basic.lean

Modified Mathlib/LinearAlgebra/Dimension/DivisionRing.lean

Modified Mathlib/LinearAlgebra/DirectSum/Finsupp.lean

Modified Mathlib/LinearAlgebra/LinearPMap.lean

Modified Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/IsDiag.lean

Modified Mathlib/LinearAlgebra/Prod.lean

Modified Mathlib/Logic/Equiv/Embedding.lean

Modified Mathlib/Logic/Equiv/Fin.lean

Modified Mathlib/MeasureTheory/Measure/Complex.lean

Modified Mathlib/NumberTheory/ArithmeticFunction.lean

Modified Mathlib/NumberTheory/DiophantineApproximation/Basic.lean

Modified Mathlib/NumberTheory/PythagoreanTriples.lean

Modified Mathlib/Order/Antisymmetrization.lean

Modified Mathlib/Order/RelIso/Basic.lean

Modified Mathlib/Order/SupIndep.lean

Modified Mathlib/Probability/Independence/Kernel.lean

Modified Mathlib/RingTheory/GradedAlgebra/Radical.lean

Modified Mathlib/RingTheory/HahnSeries/Multiplication.lean

Modified Mathlib/RingTheory/Ideal/Prod.lean

Modified Mathlib/RingTheory/Kaehler/JacobiZariski.lean

Modified Mathlib/RingTheory/MvPowerSeries/Basic.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

Modified Mathlib/SetTheory/Cardinal/Finite.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean

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

Modified Mathlib/Topology/FiberBundle/Basic.lean

Modified Mathlib/Topology/FiberBundle/Constructions.lean

Modified Mathlib/Topology/Gluing.lean

Modified Mathlib/Topology/Homotopy/HSpaces.lean

Modified Mathlib/Topology/Instances/ENNReal/Lemmas.lean

Modified Mathlib/Topology/VectorBundle/Hom.lean