Def RestrictedProduct.evalRingHom

Modification history

2025-06-10 22:59

Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean

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

Modified RestrictedProduct.evalRingHom View on Github →

2025-04-23 16:26

Mathlib/Topology/Algebra/RestrictedProduct.lean

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

Added RestrictedProduct.evalRingHom View on Github →