Commit 2025-06-06 08:51 22d804d2

View on Github →

fix: rename ContinuousLinearEquiv.prod to prodCongr (#25513) This matches Equiv.prodCongr and LinearEquiv.prodCongr.

Estimated changes

Modified Mathlib/Analysis/Convolution.lean

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

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

deleted theorem ContinuousLinearEquiv.coe_prod

added theorem ContinuousLinearEquiv.coe_prodCongr

deleted def ContinuousLinearEquiv.prod

added def ContinuousLinearEquiv.prodCongr

added theorem ContinuousLinearEquiv.prodCongr_apply

added theorem ContinuousLinearEquiv.prodCongr_symm

deleted theorem ContinuousLinearEquiv.prod_apply

deleted theorem ContinuousLinearEquiv.prod_symm

Modified Mathlib/Topology/VectorBundle/Constructions.lean