Def RestrictedProduct.mapRingHom

Modification history

2025-07-31 19:52

Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean

feat: more RestrictedProduct API (#25715) …

Deleted RestrictedProduct.mapRingHom View on Github →

2025-06-10 22:59

Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean

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

Modified RestrictedProduct.mapRingHom View on Github →

2025-04-23 16:26

Mathlib/Topology/Algebra/RestrictedProduct.lean

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

Added RestrictedProduct.mapRingHom View on Github →