Def RestrictedProduct.evalMonoidHom

Modification history

2025-06-10 22:59

Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean

chore: split Mathlib/Topology/Algebra/RestrictedProduct (#25558) …

Modified RestrictedProduct.evalMonoidHom View on Github →

2025-04-23 16:26

Mathlib/Topology/Algebra/RestrictedProduct.lean

feat (Topology/Algebra/RestrictedProduct): add API (#24200) …

Added RestrictedProduct.evalMonoidHom View on Github →