Commit 2025-04-23 16:26 7b91fb07

View on Github →

feat (Topology/Algebra/RestrictedProduct): add API (#24200) In this PR we add ext, eval and map API for RestrictedProduct.

Estimated changes

Modified Mathlib/Topology/Algebra/RestrictedProduct.lean

added def RestrictedProduct.evalMonoidHom

added theorem RestrictedProduct.evalMonoidHom_apply

added def RestrictedProduct.evalRingHom

added theorem RestrictedProduct.evalRingHom_apply

added theorem RestrictedProduct.ext

added def RestrictedProduct.map

added def RestrictedProduct.mapMonoidHom

added theorem RestrictedProduct.mapMonoidHom_apply

added def RestrictedProduct.mapRingHom

added theorem RestrictedProduct.mapRingHom_apply

added theorem RestrictedProduct.map_apply

modified theorem RestrictedProduct.range_coe_principal