Commit 2025-07-31 19:52 c604c957

View on Github →

feat: more RestrictedProduct API (#25715) A constructor, more algebra boilerplate (e.g. SMul ℕ on a restricted product of AddMonoids, restricted product of CommMonoids is a CommMonoid, restricted product of R-modules wrt R-submodules is an R-module, variant of map when the index set doesn't change). From the FLT project.

Estimated changes

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

added def RestrictedProduct.coeMonoidHom

modified def RestrictedProduct.map

added def RestrictedProduct.mapAlong

added def RestrictedProduct.mapAlongMonoidHom

added theorem RestrictedProduct.mapAlongMonoidHom_apply

added def RestrictedProduct.mapAlongRingHom

added theorem RestrictedProduct.mapAlongRingHom_apply

added theorem RestrictedProduct.mapAlong_apply

deleted def RestrictedProduct.mapMonoidHom

deleted theorem RestrictedProduct.mapMonoidHom_apply

deleted def RestrictedProduct.mapRingHom

deleted theorem RestrictedProduct.mapRingHom_apply

modified theorem RestrictedProduct.map_apply

added theorem RestrictedProduct.mk_apply

Modified Mathlib/Topology/Algebra/RestrictedProduct/TopologicalSpace.lean

added theorem RestrictedProduct.mapAlong_continuous

deleted theorem RestrictedProduct.map_continuous