Commit 2025-04-19 15:05 0d9eafd4

View on Github →

chore: rename LinearEquiv.prod to prodCongr (#24145) Zulip discussion: #mathlib4 > Naming convention @ 💬 As a bonus, replace some outdated prod.map in module doc-strings by Prod.map.

Estimated changes

Modified Mathlib/Algebra/Group/Prod.lean

Modified Mathlib/Algebra/Module/PID.lean

Modified Mathlib/Analysis/Calculus/LagrangeMultipliers.lean

Modified Mathlib/Analysis/Normed/Lp/PiLp.lean

Modified Mathlib/LinearAlgebra/Basis/Prod.lean

Modified Mathlib/LinearAlgebra/Basis/VectorSpace.lean

Modified Mathlib/LinearAlgebra/Dimension/Constructions.lean

Modified Mathlib/LinearAlgebra/Prod.lean

deleted theorem LinearEquiv.coe_prod

added theorem LinearEquiv.coe_prodCongr

added theorem LinearEquiv.prodCongr_apply

added theorem LinearEquiv.prodCongr_symm

deleted theorem LinearEquiv.prod_apply

deleted theorem LinearEquiv.prod_symm

Modified Mathlib/LinearAlgebra/QuadraticForm/Dual.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Prod.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Prod.lean

Modified Mathlib/LinearAlgebra/Trace.lean

Modified Mathlib/Order/Hom/Basic.lean

Modified Mathlib/RingTheory/TensorProduct/IsBaseChangePi.lean

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