Commit 2024-01-24 14:31 00202e4a

View on Github →

feat(Topology/Support): add tsupport_smul_{left,right} (#9778)

rename Function.support_smul_subset_right to Function.support_const_smul_subset From sphere-eversion; I'm just upstreaming it.

Estimated changes

Modified Archive/Hairer.lean

Modified Mathlib/Algebra/Module/Basic.lean

added theorem Function.support_const_smul_subset

modified theorem Function.support_smul_subset_right

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

Modified Mathlib/RingTheory/HahnSeries.lean

Modified Mathlib/Topology/Support.lean

added theorem tsupport_smul_subset_right