feat: The finite product of semi-rings (in terms of measure theory) is a semi-ring.

[pfaffelh]

Move results for rings (in terms of measure theory) to a separate file; was in Semiring.lean before.
For ∀ i ∈ s, IsSetSemiring (C i)), the product s.pi '' s.pi C is a semiring.
Prove two auxiliary lemmas in Data.Set.Prod needed on the way.

[github-actions]

PR summary 3bb3ee2af4

Import changes exceeding 2%

%	File
+13.05%	Mathlib.MeasureTheory.SetSemiring

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.MeasureTheory.SetSemiring	613	693	+80 (+13.05%)
Mathlib.Data.Set.Prod	235	237	+2 (+0.85%)
Mathlib.Data.Set.Pairwise.Lattice	273	275	+2 (+0.73%)

Import changes for all files

Files	Import difference
4 files Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent Mathlib.MeasureTheory.Measure.AddContent Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.MeasureTheory.OuterMeasure.OfAddContent	1
151 files Mathlib.Algebra.Field.ULift Mathlib.Algebra.Group.Action.Pi Mathlib.Algebra.Group.Action.Pointwise.Set.Basic Mathlib.Algebra.Group.Indicator Mathlib.Algebra.Group.Pi.Lemmas Mathlib.Algebra.Group.Pointwise.Set.Basic Mathlib.Algebra.Group.Pointwise.Set.Lattice Mathlib.Algebra.Group.Pointwise.Set.Scalar Mathlib.Algebra.Group.Submonoid.Basic Mathlib.Algebra.Group.Submonoid.MulOpposite Mathlib.Algebra.Group.Submonoid.Operations Mathlib.Algebra.Group.Subsemigroup.Basic Mathlib.Algebra.Group.Subsemigroup.Membership Mathlib.Algebra.Group.Subsemigroup.Operations Mathlib.Algebra.GroupWithZero.Indicator Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic Mathlib.Algebra.Module.PointwisePi Mathlib.Algebra.NoZeroSMulDivisors.Pi Mathlib.Algebra.Order.Field.Pointwise Mathlib.Algebra.Order.Group.Action.Flag Mathlib.Algebra.Order.Group.Action Mathlib.Algebra.Order.Group.CompleteLattice Mathlib.Algebra.Order.Group.Indicator Mathlib.Algebra.Order.Group.Pointwise.Bounds Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice Mathlib.Algebra.Order.GroupWithZero.Bounds Mathlib.Algebra.Order.Interval.Set.Monoid Mathlib.Algebra.Order.Kleene Mathlib.Algebra.Order.Pi Mathlib.Algebra.Order.Quantale Mathlib.Algebra.Order.Ring.Prod Mathlib.Algebra.Ring.Action.Pointwise.Set Mathlib.Algebra.Ring.CompTypeclasses Mathlib.Algebra.Ring.Equiv Mathlib.Algebra.Ring.Pi Mathlib.Algebra.Ring.Pointwise.Set Mathlib.Algebra.Ring.Prod Mathlib.Algebra.Ring.Submonoid.Basic Mathlib.Algebra.Ring.Submonoid Mathlib.Algebra.Ring.ULift Mathlib.Algebra.Tropical.Lattice Mathlib.Combinatorics.Quiver.Arborescence Mathlib.Data.Countable.Small Mathlib.Data.FP.Basic Mathlib.Data.Int.ConditionallyCompleteOrder Mathlib.Data.List.Iterate Mathlib.Data.Nat.Pairing Mathlib.Data.PFun Mathlib.Data.Rel Mathlib.Data.Semiquot Mathlib.Data.Set.Accumulate Mathlib.Data.Set.BooleanAlgebra Mathlib.Data.Set.Function Mathlib.Data.Set.Functor Mathlib.Data.Set.Lattice.Image Mathlib.Data.Set.Lattice Mathlib.Data.Set.Monotone Mathlib.Data.Set.NAry Mathlib.Data.Set.Pairwise.Basic Mathlib.Data.Set.Pairwise.Lattice Mathlib.Data.Set.Piecewise Mathlib.Data.Set.Prod Mathlib.Data.Set.Sigma Mathlib.Data.Set.Subset Mathlib.Data.Set.UnionLift Mathlib.Data.Setoid.Basic Mathlib.GroupTheory.Congruence.Basic Mathlib.GroupTheory.Congruence.Defs Mathlib.GroupTheory.Congruence.Hom Mathlib.GroupTheory.Congruence.Opposite Mathlib.GroupTheory.GroupAction.DomAct.ActionHom Mathlib.GroupTheory.GroupAction.DomAct.Basic Mathlib.GroupTheory.GroupAction.Embedding Mathlib.GroupTheory.GroupAction.Pointwise Mathlib.GroupTheory.GroupAction.Support Mathlib.GroupTheory.Submonoid.Center Mathlib.GroupTheory.Submonoid.Centralizer Mathlib.GroupTheory.Subsemigroup.Centralizer Mathlib.Logic.Equiv.Nat Mathlib.Logic.Equiv.PartialEquiv Mathlib.Logic.Equiv.Set Mathlib.Logic.Small.Basic Mathlib.Logic.Small.Set Mathlib.Order.Antichain Mathlib.Order.Bounds.Image Mathlib.Order.Bounds.Lattice Mathlib.Order.Bounds.OrderIso Mathlib.Order.Chain Mathlib.Order.Closure Mathlib.Order.Cofinal Mathlib.Order.CompleteBooleanAlgebra Mathlib.Order.CompleteLattice.Basic Mathlib.Order.CompleteLattice.Chain Mathlib.Order.CompleteLattice.Lemmas Mathlib.Order.Concept Mathlib.Order.ConditionallyCompleteLattice.Basic Mathlib.Order.ConditionallyCompleteLattice.Defs Mathlib.Order.ConditionallyCompleteLattice.Group Mathlib.Order.ConditionallyCompleteLattice.Indexed Mathlib.Order.Copy Mathlib.Order.Extension.Linear Mathlib.Order.Filter.AtTopBot.Basic Mathlib.Order.Filter.AtTopBot.CompleteLattice Mathlib.Order.Filter.AtTopBot.Defs Mathlib.Order.Filter.AtTopBot.Disjoint Mathlib.Order.Filter.AtTopBot.Field Mathlib.Order.Filter.AtTopBot.Group Mathlib.Order.Filter.AtTopBot.Map Mathlib.Order.Filter.AtTopBot.Monoid Mathlib.Order.Filter.AtTopBot.Ring Mathlib.Order.Filter.AtTopBot.Tendsto Mathlib.Order.Filter.Bases.Basic Mathlib.Order.Filter.Basic Mathlib.Order.Filter.Curry Mathlib.Order.Filter.Ker Mathlib.Order.Filter.Map Mathlib.Order.Filter.NAry Mathlib.Order.Filter.Partial Mathlib.Order.Filter.Prod Mathlib.Order.Filter.Tendsto Mathlib.Order.GaloisConnection.Basic Mathlib.Order.Heyting.Regular Mathlib.Order.Hom.CompleteLattice Mathlib.Order.Hom.Order Mathlib.Order.Hom.Set Mathlib.Order.Interval.Basic Mathlib.Order.Interval.Set.Disjoint Mathlib.Order.Interval.Set.Image Mathlib.Order.Interval.Set.OrderIso Mathlib.Order.Interval.Set.SurjOn Mathlib.Order.Minimal Mathlib.Order.Monotone.Extension Mathlib.Order.Nucleus Mathlib.Order.OrdContinuous Mathlib.Order.Preorder.Chain Mathlib.Order.Rel.GaloisConnection Mathlib.Order.RelIso.Set Mathlib.Order.SemiconjSup Mathlib.Order.WellFounded Mathlib.Order.Zorn Mathlib.RingTheory.Congruence.Basic Mathlib.RingTheory.Congruence.Defs Mathlib.RingTheory.Congruence.Opposite Mathlib.RingTheory.RingInvo Mathlib.SetTheory.ZFC.PSet Mathlib.Tactic.DeriveCountable Mathlib.Tactic.Monotonicity.Lemmas Mathlib.Tactic.Monotonicity Mathlib.Tactic.Peel Mathlib.Topology.Defs.Filter Mathlib.Topology.Defs.Sequences	2
Mathlib.MeasureTheory.SetAlgebra Mathlib.MeasureTheory.SetSemiring	80

---

Declarations diff

+ IsPiSystem.pi_subset
+ disjoint_pi_of_interSetdiff_of_interSetdiffInter
+ fintype_pi_ofFinset
+ iff
+ isPiSystem_iff_of_nmem_empty
+ pairwiseDisjoint_set_pi
+ pairwiseDisjoint_union_of_disjoint
+ pi
+ pi_antitone
+ pi_inter_image
+ pi_inter_image'
+ pi_setdiff_eq_union
+ pi_singleton_diff_eq_sUnion
+ subset_pi_image_of_subset
+ union_pi_ite_of_disjoint

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[leanprover-community-bot-assistant]

This pull request has conflicts, please merge master and resolve them.

[RemyDegenne]

Closing: replaced by #25902