Commit 2024-11-04 13:07 375af59c

View on Github →

chore: split Topology/ContinuousMap/Algebra (#18604) I picked this from rg -c "^import" | sort -k2 -t: -n | tail -50, i.e. the files in Mathlib with the most direct imports.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

Modified Mathlib/Analysis/Fourier/PoissonSummation.lean

Modified Mathlib/MeasureTheory/Measure/Haar/Unique.lean

Modified Mathlib/Topology/ContinuousMap/Algebra.lean

deleted theorem ContinuousMap.coe_mabs

deleted theorem ContinuousMap.coe_star

deleted def ContinuousMap.compStarAlgHom'

deleted theorem ContinuousMap.compStarAlgHom'_comp

deleted theorem ContinuousMap.compStarAlgHom'_id

deleted def ContinuousMap.compStarAlgHom

deleted theorem ContinuousMap.compStarAlgHom_comp

deleted theorem ContinuousMap.compStarAlgHom_id

deleted def ContinuousMap.evalStarAlgHom

deleted theorem ContinuousMap.mabs_apply

deleted theorem ContinuousMap.periodic_tsum_comp_add_zsmul

deleted theorem ContinuousMap.star_apply

deleted def Homeomorph.compStarAlgEquiv'

Modified Mathlib/Topology/ContinuousMap/Compact.lean

Created Mathlib/Topology/ContinuousMap/Lattice.lean

added theorem ContinuousMap.coe_mabs

added theorem ContinuousMap.mabs_apply

Created Mathlib/Topology/ContinuousMap/Periodic.lean

added theorem ContinuousMap.periodic_tsum_comp_add_zsmul

Modified Mathlib/Topology/ContinuousMap/Polynomial.lean

Created Mathlib/Topology/ContinuousMap/Star.lean

added theorem ContinuousMap.coe_star

added def ContinuousMap.compStarAlgHom'

added theorem ContinuousMap.compStarAlgHom'_comp

added theorem ContinuousMap.compStarAlgHom'_id

added def ContinuousMap.compStarAlgHom

added theorem ContinuousMap.compStarAlgHom_comp

added theorem ContinuousMap.compStarAlgHom_id

added def ContinuousMap.evalStarAlgHom

added theorem ContinuousMap.star_apply

added def Homeomorph.compStarAlgEquiv'

Modified Mathlib/Topology/ContinuousMap/StarOrdered.lean

Modified Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean

Modified Mathlib/Topology/PartitionOfUnity.lean