Theorem RestrictedProduct.exists_structureMap_eq_of_forall

Modification history

2025-06-10 22:59
Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean
chore: split Mathlib/Topology/Algebra/RestrictedProduct (#25558) …
Modified RestrictedProduct.exists_structureMap_eq_of_forallView on Github →
2025-03-17 22:05
Mathlib/Topology/Algebra/RestrictedProduct.lean
feat: restricted products and their topology (#20021)
Added RestrictedProduct.exists_structureMap_eq_of_forallView on Github →