Commit 2025-11-06 11:49 efdba040

View on Github →

chore(*): use autoparams and fun_prop (#31317)

Estimated changes

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

Modified Mathlib/Analysis/Complex/Circle.lean

modified theorem Real.continuous_probChar

Modified Mathlib/Analysis/Fourier/AddCircleMulti.lean

Modified Mathlib/Condensed/Light/TopCatAdjunction.lean

Modified Mathlib/Condensed/TopCatAdjunction.lean

Modified Mathlib/Topology/Category/CompHausLike/Limits.lean

Modified Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean

Modified Mathlib/Topology/ContinuousMap/ZeroAtInfty.lean

Modified Mathlib/Topology/PartitionOfUnity.lean

Modified Mathlib/Topology/TietzeExtension.lean

Modified Mathlib/Topology/UrysohnsLemma.lean