Theorem RestrictedProduct.mapRingHom_apply

Modification history

2025-07-31 19:52
Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean
feat: more RestrictedProduct API (#25715) …
Deleted RestrictedProduct.mapRingHom_applyView on Github →
2025-06-10 22:59
Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean
chore: split Mathlib/Topology/Algebra/RestrictedProduct (#25558) …
Modified RestrictedProduct.mapRingHom_applyView on Github →
2025-04-23 16:26
Mathlib/Topology/Algebra/RestrictedProduct.lean
feat (Topology/Algebra/RestrictedProduct): add API (#24200) …
Added RestrictedProduct.mapRingHom_applyView on Github →