Mathlib Changelog
v4
Changelog
About
Github
Theorem
RestrictedProduct.mapAlongRingHom_apply
Modification history
2025-07-31 19:52
Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean
feat: more RestrictedProduct API (#25715) …
Added
RestrictedProduct.mapAlongRingHom_apply
View on Github →