Theorem RestrictedProduct.ext

Modification history

2025-07-04 07:44

Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean

chore: further whitespace fixes (#26708) …

Modified RestrictedProduct.ext View on Github →

2025-06-10 22:59

Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean

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

Modified RestrictedProduct.ext View on Github →

2025-04-23 16:26

Mathlib/Topology/Algebra/RestrictedProduct.lean

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

Added RestrictedProduct.ext View on Github →