Commit 2024-12-11 17:56 ca6f586b

View on Github →

chore(*): fix initialize_simps_projections commands (#19422) With old configs, @[simps] generated both _toFun and _apply lemmas.

Estimated changes

Modified Mathlib/Algebra/Order/AbsoluteValue.lean

Modified Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean

Modified Mathlib/Analysis/Normed/Operator/LinearIsometry.lean

Modified Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean

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

Modified Mathlib/MeasureTheory/Measure/Portmanteau.lean

Modified Mathlib/NumberTheory/Padics/MahlerBasis.lean

Modified Mathlib/Topology/Algebra/Algebra.lean

Modified Mathlib/Topology/Algebra/Module/Basic.lean

Modified Mathlib/Topology/ContinuousMap/Bounded/Basic.lean

added theorem BoundedContinuousFunction.coe_toContinuousMap

deleted theorem BoundedContinuousFunction.coe_to_continuous_fun

Modified Mathlib/Topology/ContinuousMap/Ideals.lean

Modified Mathlib/Topology/Homotopy/Basic.lean

Modified Mathlib/Topology/MetricSpace/Isometry.lean