Commit 2025-10-23 10:10 98b14016

View on Github →

chore: generalize tprod_ite_eq (#30810)

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/l2Space.lean

Modified Mathlib/Probability/ProbabilityMassFunction/Monad.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

modified theorem tprod_ite_eq