Commit 2026-03-13 18:00 7564c5ab

View on Github →

feat: generalize some ContinuousMul hypotheses to SeparatelyContinuousMul (#36562) As discussed at [#mathlib4 > A `ContinuousConstMul` class @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/A.20.60ContinuousConstMul.60.20class/near/578259560)

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

Modified Mathlib/MeasureTheory/Measure/Content.lean

modified theorem MeasureTheory.Content.is_mul_left_invariant_innerContent

modified theorem MeasureTheory.Content.is_mul_left_invariant_outerMeasure

Modified Mathlib/Topology/Algebra/Algebra/Rat.lean

Modified Mathlib/Topology/Algebra/Constructions.lean

Modified Mathlib/Topology/Algebra/Field.lean

modified theorem Filter.tendsto_cocompact_mul_left₀

modified theorem Filter.tendsto_cocompact_mul_right₀

Modified Mathlib/Topology/Algebra/Group/ClosedSubgroup.lean

Modified Mathlib/Topology/Algebra/Group/Quotient.lean

Modified Mathlib/Topology/Algebra/GroupWithZero.lean

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

Modified Mathlib/Topology/Algebra/OpenSubgroup.lean

modified theorem OpenSubgroup.isClopen

modified theorem OpenSubgroup.isClosed

modified theorem Subgroup.discreteTopology

modified theorem Subgroup.isClosed_of_isOpen

modified theorem Subgroup.isOpen_mono

modified theorem Subgroup.isOpen_of_mem_nhds

modified theorem Subgroup.isOpen_of_one_mem_interior

modified theorem Subgroup.quotient_finite_of_isOpen

Modified Mathlib/Topology/ApproximateUnit.lean

modified theorem Filter.IsApproximateUnit.iff_le_nhds_one

modified theorem Filter.IsApproximateUnit.iff_neBot_and_le_nhds_one

modified theorem Filter.IsApproximateUnit.nhds_one

Modified Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean