Commit 2025-08-28 12:31 4ee73c03

View on Github →

feat: measurable_from_prod_countable_right (#28547)

Estimated changes

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

Modified Mathlib/MeasureTheory/Group/Arithmetic.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean

deleted theorem measurable_from_prod_countable'

deleted theorem measurable_from_prod_countable

added theorem measurable_from_prod_countable_left'

added theorem measurable_from_prod_countable_left

added theorem measurable_from_prod_countable_right'

added theorem measurable_from_prod_countable_right

Modified Mathlib/Probability/Kernel/Disintegration/Basic.lean

Modified Mathlib/Probability/Kernel/Disintegration/Density.lean

Modified Mathlib/Probability/Kernel/RadonNikodym.lean

Modified scripts/nolints_prime_decls.txt