Theorem RestrictedProduct.one_apply

Modification history

2025-06-10 22:59
Mathlib/Topology/Algebra/RestrictedProduct/Basic.lean
chore: split Mathlib/Topology/Algebra/RestrictedProduct (#25558) …
Modified RestrictedProduct.one_applyView on Github →
2025-06-07 01:53
Mathlib/Topology/Algebra/RestrictedProduct.lean
Add simp lemmas for restricted product operations (#25462)
Added RestrictedProduct.one_applyView on Github →