Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-05-19 17:03
cdc2dfdd
View on Github →
chore: call
dsimp
in the default tactic of
ContinuousLinearMap
(
#37386
)
Estimated changes
Modified
Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean
Modified
Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
Modified
Mathlib/Analysis/Distribution/DerivNotation.lean
Modified
Mathlib/Analysis/Distribution/TestFunction.lean
Modified
Mathlib/Analysis/Fourier/Notation.lean
Modified
Mathlib/Analysis/InnerProductSpace/PiL2.lean
Modified
Mathlib/Analysis/Normed/Algebra/Spectrum.lean
Modified
Mathlib/Analysis/Normed/Lp/PiLp.lean
Modified
Mathlib/Analysis/Normed/Lp/ProdLp.lean
Modified
Mathlib/Analysis/Normed/Module/WeakDual.lean
Modified
Mathlib/Analysis/RCLike/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/ConjSqrt.lean
Modified
Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
Modified
Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
Modified
Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
Modified
Mathlib/Probability/Distributions/Fernique.lean
Modified
Mathlib/Probability/Distributions/Gaussian/IsGaussianProcess/Basic.lean
Modified
Mathlib/Probability/Distributions/Gaussian/IsGaussianProcess/Independence.lean
Modified
Mathlib/Topology/Algebra/Algebra.lean
Modified
Mathlib/Topology/Algebra/GroupCompletion.lean
Modified
Mathlib/Topology/Algebra/LinearMapCompletion.lean
Modified
Mathlib/Topology/Algebra/Module/Alternating/Topology.lean
Modified
Mathlib/Topology/Algebra/Module/LinearMap.lean
modified
def
ContinuousLinearMap.smulRight
Modified
Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean
modified
def
ContinuousLinearMap.coprod
modified
def
ContinuousLinearMap.pi
modified
def
ContinuousLinearMap.proj
Modified
Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean
Modified
Mathlib/Topology/Algebra/Module/Multilinear/Topology.lean
Modified
Mathlib/Topology/Algebra/Module/Star.lean
Modified
Mathlib/Topology/Algebra/Star/LinearMap.lean
Modified
Mathlib/Topology/CompactOpen.lean
Modified
Mathlib/Topology/Constructions.lean
Modified
Mathlib/Topology/ContinuousMap/Algebra.lean
Modified
Mathlib/Topology/ContinuousMap/Ideals.lean
Modified
Mathlib/Topology/Instances/TrivSqZeroExt.lean