Commit 2024-05-28 08:12 5239893b
View on Github →chore(Mathlib/Algebra/BigOperators/Basic): unscope ∑ x ∈ s, f x
notations (#13271)
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Unscoping.20big.20operators
chore(Mathlib/Algebra/BigOperators/Basic): unscope ∑ x ∈ s, f x
notations (#13271)
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Unscoping.20big.20operators