mathlib4

feat(Algebra/Star/Basic): `StarAddMonoid.toStarModule{Nat,Int}` doesn't need commutativity (#36348)

feat(dsimp%): throw an error when no progress is made (#36384)

feat: integrability with respect to a countable sum of measures (#36355)

feat(Analysis): a closed convex set is the intersection of countably many half-spaces (#31180)

chore(RepresentationTheory/Intertwining): Revert #35100 (#36394)