Commit 2025-07-26 23:35 fee05eef

feat(MeasureTheory/SimpleFunc): add instances of algebraic structures (#27336) This adds a Star instance on simple functions into a type with a star structure, the associated coe_star lemma, and the relevant algebraic compatibility instances (e.g., StarMul) when the codomain is equipped with these. We also add several missing instances (mostly Ring-like and Algebra-like). This PR is the first in a series of small PRs aimed at providing a CStarAlgebra instance for L^∞ functions.